[isabelle-dev] Feedback from a Isabelle tutorial
makarius at sketis.net
Mon Jun 27 14:11:07 CEST 2011
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
> is meant to tell Metis to be quiet, but somehow it is ignored. If you do
> lemma "map f  = "
> using map.simps
> 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
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.
More information about the isabelle-dev