[isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] "Proof terms" section of isar-ref; Outermost quantifiers
- From: gottfried.barrow at gmx.com
- Date: Fri, 08 Jun 2012 10:33:11 -0500
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
In Krauss & Schropp's "A Mechanized Translation from Higher-Order Logic
to Set Theory", page 5, <http://home.in.tum.de/~schropp/>, they say:
In Isabelle, outermost quantiers and the [.]-embedding are not
QUESTION 1: Is there a command to show these hidden meta-logic
quantifiers, or any other such hidden meta-logic? I suppose not.
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and