[isabelle-dev] Feedback from a Isabelle tutorial

[Jasmin Blanchette]

>> you get the warning
>> 
>>   ### Metis: Unused theorems: "List.map.simps_2"
>> 
>> which is strange because in Metis's code that warning is only printed if "verbose" is true. Is "Proof.map_context" not the thing I should be using?
> 
> Proof.map_context is right, also the use of the context later on, as far as I can see in the sources.
> 
> In fact, I cannot reproduce the above problem in Isabelle/0d78c8d31d0d.

OK, I now understand what went wrong. I have a special hackish setup for loading Metis and Sledgehammer, which I often use without even thinking about it, and the problem was related to that. I'm glad the issue doesn't exist after all -- it's been on my TODO list for several months now. ;)

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.

Jasmin