[isabelle] Tracing the simplifier in proofs


I would like to be able to trace a particular call to the simp method within a proof, without having to manually turn tracing on and off from the ProofGeneral menu. This is because half the time I forget to turn tracing back off when I'm replaying earlier parts of my theory, and then PG gets swamped trying to display all the calls to the various simp methods.

I tried this series of commands within my proof:

  ML "trace_simp := true"
  apply simp
  ML "trace_simp := false"

but I get the following error from Isabelle when trying to execute the first ML command:

  *** Illegal application of command "ML" in proof mode
  *** At command "ML".

So, what is the right way to be able to wrap calls to simp and auto within proofs to turn on and off tracing?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.