Re: [isabelle] Tracing the simplifier in proofs



Thanks, Florian and Makarius. I'll switch to using ML_command in proofs.

-john

On Dec 2, 2008, at 11:18 AM, Makarius wrote:

On Tue, 2 Dec 2008, John Matthews wrote:

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?

Either via the Proof General settings menu, or by issuing 'ML_command'
yourself, not 'ML'.

The reason why 'ML' did not work above is that it is now a theory command,
and cannot be used inside a proof.  This is required because you would
usually expect to allow bind_thm inside 'ML' but that updates the theory. In the next release even plain ML value bindings will affect the theory.


	Makarius






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