[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"
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