Re: [isabelle] isabelle/jedit



> 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.

Yannick,

I am not a constructivist.

And, I could accept that a menu entry would insert a forty letter long
identifier in the proof text. My concern is usability, not theoretical
elegance. Coming up with a proof is a challenging task in itself, and
it is better that the user interface helps creating it, and you need
not remember technicalities in order to advance your proof.

What do the developers think?

- Gergely





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