Re: [isabelle] Feature suggestions: More useful output

On Fri, 23 Nov 2012, Joachim Breitner wrote:

A command that does not provide any output at all is “lemma” (and also “lemmas”). Sometimes, I feel the need to check how Isabelle actually sees the lemma, e.g. to see what types she has inferred, or to check whether I am really done or if there is still a [!] behind the lemma¹. Currently, I have to use “thm name” after the lemma for that (and give the lemma a name if it does not have one yet). Would it be possible to have the lemma command already print that information?

This is in a transitional state, between old TTY things that no longer work, and proper global status summaries in the Prover IDE.

Conceptually, the internal derivation object cannot be displayed to the user while editing and asynchronous/parallel checking continues. I've no particular plans for the coming release here -- too many other things need to be consolidated first.


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