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