# [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
printed...

`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?
`
Thanks
GB

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