[isabelle-dev] A suggestion: call eval with try0

Dr A. Koutsoukou-Argyraki ak2110 at cam.ac.uk
Sat Aug 15 15:57:13 CEST 2020

Dear all,

eval is not one of the many methods called by try0, and to my experience 
so far Sledgehammer doesn't suggest it either.
I've noticed several very simple proofs that work just "by eval" and yet 
automation won't suggest any proof.

Do people agree that it would be practical to include eval in the 
methods tried with try0?

and would this be feasible ?

Best wishes,

More information about the isabelle-dev mailing list