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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
