*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Tracing the simplifier in proofs*From*: John Matthews <matthews at galois.com>*Date*: Wed, 3 Dec 2008 12:49:46 -0800*In-reply-to*: <Pine.LNX.4.64.0812022016120.13186@macbroy20.informatik.tu-muenchen.de>*References*: <5C28FB81-B020-4926-89A9-9069D7FCAE9E@galois.com> <Pine.LNX.4.64.0812022016120.13186@macbroy20.informatik.tu-muenchen.de>

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 executethe firstML 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 autowithinproofs 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 theorycommand,and cannot be used inside a proof. This is required because you wouldusually expect to allow bind_thm inside 'ML' but that updates thetheory.In the next release even plain ML value bindings will affect thetheory.Makarius

**References**:**[isabelle] Tracing the simplifier in proofs***From:*John Matthews

**Re: [isabelle] Tracing the simplifier in proofs***From:*Makarius

- Previous by Date: Re: [isabelle] Tracing the simplifier in proofs
- Next by Date: [isabelle] mod_mult_distrib
- Previous by Thread: Re: [isabelle] Tracing the simplifier in proofs
- Next by Thread: [isabelle] mod_mult_distrib
- Cl-isabelle-users December 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list