Re: [isabelle] Feature Request



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.