[isabelle] Feature Request



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





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