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. Tobias 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) > > Cheers, > Gerwin > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
