Re: [isabelle] Feature suggestion: Replace statement by pretty-printed statement

On Tue, 6 May 2014, Julian Brunner wrote:

On Wed, Apr 30, 2014 at 11:54 AM, Tobias Nipkow <nipkow at> wrote:
Although I do not do this editing that Joachim describes, I also sometimes
wish that defnitions and lemmas would print the proposition to see what it
looks like.

Definitions and the final proof steps of theorem statements don't have any print output yet, so there's an unused opportunity to provide information. The final proof steps of have, show and obtain statements in isar proofs already do this, too.

There is a long and thorny history behind certain variations of printing of "state" or "results" -- in TTY mode, Proof General 2.x, 3.x, 4.x, even Isabelle/jEdit with its 5 years. I have looked a bit through all that once again, and there is a good chance that it will be more smooth in the coming release -- not every detail from the past needs to be retained today.

When the Isabelle2014-RC phase starts, presumably in July, you should take the opportunity to make a serious test of the many new things that have accumulated.


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