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.


	Makarius





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