[isabelle-dev] NEWS: find_theorems solves

[Tobias Nipkow]

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