Jasmin Blanchette wrote:
This motivates me to attack the "linarith" problem. If nobody objects, I'll call the property "linarith_verbose" and have it on by default (for compatibility) but off in "try_methods" and "try". I've also taken the liberty to reword the "counterexample trace" message to make it clear that the counterexample might be spurious.
Adding such a flag is certainly helpful, and I was considering to do exactly that, but you're obviously faster.
Anyway, Tobias and me briefly discussed to reduce the number of linarith messages dramatically as most counterexamples are actually none. This will be addressed by us in the near future.
Cheers, Sascha _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
