Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Feature Request

Email Gateway (Aug 18 2022 at 14:36):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,

some time ago I was wondering about how to present proofs (in
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-January/msg00037.html)
in papers. Since then I use the method proposed by Jesper
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-January/msg00043.html);
thanks btw.

...

okay first I wanted to go for Larry's suggestion and not use document
preparation at all... but then I got ambitious :)

However, typing lines like

"s \<^raw:\rstep{>R\<^raw:}> t"

instead of

"s ->R t"

is really awkward. In the current setting it seems to me, as if only
thoerems (i.e., the results after a proof) but not the proofs itself are
nicely supported for document preparation. This is a pity, since the
otherwise very comfortable Isar is somehow damped down.

Is it planned to also apply 'notation's to statements inside proofs at
some point? And if not, what are the reasons?

cheers

chris

Email Gateway (Aug 18 2022 at 14:37):

From: Alexander Krauss <krauss@in.tum.de>
Hi Chris,

.. but then I got ambitious :)
[...]

"s \<^raw:\rstep{>R\<^raw:}> t"

This looks indeed ambitious :-)

In the current setting it seems to me, as if only
thoerems (i.e., the results after a proof) but not the proofs itself are
nicely supported for document preparation. This is a pity, since the
otherwise very comfortable Isar is somehow damped down.

Is it planned to also apply 'notation's to statements inside proofs at
some point? And if not, what are the reasons?

It is very difficult to do, due to constraints in the current
architecture. Isar source text has no concrete representation in the
system, so at the point where enough information is available to
pretty-print the terms, the rest of the text is already lost.

Since the new UI paradigm is based on sources being annotated with
semantic information coming from the prover, this will probably be part
of the long-term solution...

Alex

Last updated: Apr 27 2024 at 04:17 UTC