[isabelle-dev] Feedback from a Isabelle tutorial

[boehmes at mailbroy.informatik.tu-muenchen.de]

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