[isabelle] Tracing the simplifier in proofs



Hi,

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?

Thanks,
-john







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