src/Pure/Pure.thy
 changeset 26958 ed3a58a9eae1 parent 26572 9178a7f4c4c8 child 27681 8cedebf55539
```     1.1 --- a/src/Pure/Pure.thy	Sun May 18 17:03:20 2008 +0200
1.2 +++ b/src/Pure/Pure.thy	Sun May 18 17:03:23 2008 +0200
1.3 @@ -14,14 +14,14 @@
1.4  lemmas meta_impE = meta_mp [elim_format]
1.5
1.6  lemma meta_spec:
1.7 -  assumes "!!x. PROP P(x)"
1.8 -  shows "PROP P(x)"
1.9 -    by (rule `!!x. PROP P(x)`)
1.10 +  assumes "!!x. PROP P x"
1.11 +  shows "PROP P x"
1.12 +    by (rule `!!x. PROP P x`)
1.13
1.14  lemmas meta_allE = meta_spec [elim_format]
1.15
1.16  lemma swap_params:
1.17 -  "(!!x y. PROP P(x, y)) == (!!y x. PROP P(x, y))" ..
1.18 +  "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
1.19
1.20
1.21  subsection {* Embedded terms *}
1.22 @@ -39,22 +39,22 @@
1.23
1.24  lemma all_conjunction:
1.25    includes meta_conjunction_syntax
1.26 -  shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
1.27 +  shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
1.28  proof
1.29 -  assume conj: "!!x. PROP A(x) && PROP B(x)"
1.30 -  show "(!!x. PROP A(x)) && (!!x. PROP B(x))"
1.31 +  assume conj: "!!x. PROP A x && PROP B x"
1.32 +  show "(!!x. PROP A x) && (!!x. PROP B x)"
1.33    proof -
1.34      fix x
1.35 -    from conj show "PROP A(x)" by (rule conjunctionD1)
1.36 -    from conj show "PROP B(x)" by (rule conjunctionD2)
1.37 +    from conj show "PROP A x" by (rule conjunctionD1)
1.38 +    from conj show "PROP B x" by (rule conjunctionD2)
1.39    qed
1.40  next
1.41 -  assume conj: "(!!x. PROP A(x)) && (!!x. PROP B(x))"
1.42 +  assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
1.43    fix x
1.44 -  show "PROP A(x) && PROP B(x)"
1.45 +  show "PROP A x && PROP B x"
1.46    proof -
1.47 -    show "PROP A(x)" by (rule conj [THEN conjunctionD1, rule_format])
1.48 -    show "PROP B(x)" by (rule conj [THEN conjunctionD2, rule_format])
1.49 +    show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
1.50 +    show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
1.51    qed
1.52  qed
1.53
```