On Sun, 26 Jun 2011, Jasmin Christian Blanchette wrote:
Now, this all sounds well and good, but there is a little glitch. In
"try_methods.ML" the line
val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose
false)
is meant to tell Metis to be quiet, but somehow it is ignored. If you do
lemma "map f [] = []"
using map.simps
try_methods
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
