>> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
