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



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 quantiers 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.