Re: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers

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

In looking for such a command, I was looking at the "prf" command on page 141 of 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 the current object logic?

The FOL and HOL-Proofs images have proof terms already included. You can say something like "Isabelle2012/build FOL" or "Isabelle2012/build -m HOL-Proofs" in the terminal; the latter takes quite long.

Once your session is up and running with one of these images, you need to enable proof terms again for your interactive session, e.g. like this:

  ML {* proofs := 2 *}

Unfortunately, the manuals and the system are not in best shape for proof terms, because they are so rarely used.

Some examples are in src/HOL/Proofs/.


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