*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers*From*: Makarius <makarius at sketis.net>*Date*: Thu, 28 Jun 2012 23:33:54 +0200 (CEST)*Cc*: gottfried.barrow at gmx.com*In-reply-to*: <4FD21B37.8010304@gmx.com>*References*: <4FD21B37.8010304@gmx.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 8 Jun 2012, gottfried.barrow at gmx.com wrote:

In looking for such a command, I was looking at the "prf" command on page 141of isar-ref.pdf. It says:Note that this requires proof terms to be switched on for the current object logic (see the "Proof terms" section of the Isabelle reference manual for information on how to do this).I did searches, looked around, and looked in the index of isar-ref.pdf,but I never found any "Proof terms" section that gave such information.QUESTION 2: Where does it tell me how to switch on proof terms for thecurrent object logic?

ML {* proofs := 2 *}

Some examples are in src/HOL/Proofs/. Makarius

**Follow-Ups**:**Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers***From:*Gottfried Barrow

**References**:**[isabelle] "Proof terms" section of isar-ref; Outermost quantifiers***From:*gottfried . barrow

- Previous by Date: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Next by Date: Re: [isabelle] jEdit: -l flag
- Previous by Thread: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Next by Thread: Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- Cl-isabelle-users June 2012 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