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

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

```
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.
```
There two different things here:

(1) Outermost quantifiers are circumvented, by writing things with fixed
variables instead ("eigen context") and then make them arbitrary in
the result.

If you do write explicit quantifiers, which are escpecially required
for things nested on the LHS (e.g. in assumptions), there is an
explicit core inference that removes the quantifiers and expresses the
generality in terms of schematic variables.

Examples:

theorem "x = y ==> y = z ==> x = z" by (rule trans)
theorem "⋀x y z. x = y ==> y = z ==> x = z" by (rule trans)

Note that this stripping of outermost quantifiers looses some
information, but it is convenient, and quite essential for the
implicit rule composition scheme of Isabelle.

(2) [.] is notation in the cited paper for Trueprop.  Here is a
copy-paste from an explanation that I have given in some Isabelle
course at some point:

text {*
The object-logic is embedded into the Pure framework via an implicit
derivability judgment @{term "Trueprop :: bool ⇒ prop"}.

Thus any HOL formulae appears atomic to the Pure framework, while
the rule structure outlines the corresponding proof pattern.

This can be made explicit as follows:
*}

begin
write Trueprop  ("Tr")

thm conjI
thm impI
thm nat.induct
end

```
Above you can also use a global 'notation' command, but making everything local is more fun.
```

Makarius```

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