[isabelle-dev] Feedback from a Isabelle tutorial

boehmes at mailbroy.informatik.tu-muenchen.de boehmes at mailbroy.informatik.tu-muenchen.de
Mon Jun 27 22:39:51 CEST 2011


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



More information about the isabelle-dev mailing list