[isabelle-dev] NEWS: find_theorems solves
nipkow at in.tum.de
Wed Feb 11 19:20:42 CET 2009
This is pretty cool, thanks! Novices should love it.
How about coloring its message the same way QC colors its couterexamples?
I suspect it causes too much of a delay to enable it by default?
I wish we had a model for asynchronous messages, so we could run it as
a separate thread and it would report back if it found something.
Without causing a small delay for the user.
Gerwin Klein wrote:
> * New find_theorems criterion "solves" matching theorems that
> directly solve the current goal. Try "find_theorems solves".
> * Added an auto solve option, which can be enabled through the
> ProofGeneral Isabelle settings menu (disabled by default).
> When enabled, find_theorems solves is called whenever a new lemma
> is stated. Any theorems that could solve the lemma directly are
> listed underneath the goal.
> (contributed by Timothy Bourke)
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev