# Re: [isabelle] Thanks Nitpick for actually answering a former, simple question

```On Wed, 12 Sep 2012, Gottfried Barrow wrote:

```
```On 9/11/2012 3:51 PM, Lars Noschinski wrote:
```
But the implicit all quantification happens on the outermost level of the term, which explains your examples below. They can be simplified as follows:
```"!a b. ~(P a b)"
"!a b. P a b"
"~(!a b. P a b)"
```
```
```
And Makarius had talked some about outermost quantifiers in an email, and how they get stripped away.
```
```
This was about the Pure connectives !! and ==> which are not the same as HOL ! and --> (and more), even though sometimes people prefer to smash that distinction. The point of Pure connectives is to describe the structure of a rule statement declaratively, so that the system knows what is meant and how to compose the rules (by back-chaining and unification).
```
```
This is in contrast to the usual FOL view on logic with many connectives, and application-specific operations (set-theory, lattices etc.). Automated tools turn all this object-logic material *and* the Pure !! and ==> into hash-brown, and try to serve that to the user. This often works, but is no longer Pure logic, the one underlying Isar proofs.
```
So when you state

lemma "!x y. A x --> B y"

```
your result is again compact "!x y. A x --> B y" (with its implicit Trueprop wrapping).
```
But when you state

lemma "!!x y. A x ==> B y"

```
your result is schematic "A ?x ==> B ?y". You can get the same rule by writing the statement with explicit "eigen-context" as follows:
```
lemma fixes x y assumes "A x" shows "B y"

or

lemma assumes "A x" shows "B y"

```
in most situations, where x and y are implicitly free and thus ready to be fixed at the outermost level.
```
```
In the latter two forms, the resulting rules emerge naturally, without navigating through logical connectives first.
```

Makarius

```

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