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

[Dr A. Koutsoukou-Argyraki]

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,
Angeliki