Re: [isabelle] isabelle/jedit

Welcome, Gergely,

Le Wed, 08 Aug 2012 09:03:43 +0200, Gergely Buday <gbuday at> a écrit:



Christian Sternagel writes:

4.3 Where have all the menus gone?

In Proof General many settings of Isabelle and diagnostic commands
could be con%0Cgured and
started via menus. This is currently not supported in Isabelle/jEdit.


Is there any technical reason for this?

- Gergely

If you don't mind about a tiny re-interpretation, I would say a more important question would be “is that really an issue?”. I believe there are many purely intuitionist proof by exposition of good artifacts, that the Isabelle jEdit tuple is a good one (teasing and playing with words).

Note that you have the option to set Isabelle's flag from within a theory file, ex. like writing “using [[simp_trace=true]]” in a proof body. You may hide from the produced PDF document, using a special comment syntax, like writing “(*<*)using [[simp_trace=true]](*>*)”. By the way, I believe there may be a tiny issue with the simp_trace flags, … will open a thread about it later.


“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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