Re: [isabelle] Tracing the simplifier in proofs
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and