src/Pure/Pure.thy
changeset 26572 9178a7f4c4c8
parent 26570 dbc458262f4c
child 26958 ed3a58a9eae1
     1.1 --- a/src/Pure/Pure.thy	Mon Apr 07 21:25:22 2008 +0200
     1.2 +++ b/src/Pure/Pure.thy	Mon Apr 07 21:29:46 2008 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  lemmas meta_allE = meta_spec [elim_format]
     1.5  
     1.6  lemma swap_params:
     1.7 -  "(\<And>x y. PROP P(x, y)) == (\<And>y x. PROP P(x, y))" ..
     1.8 +  "(!!x y. PROP P(x, y)) == (!!y x. PROP P(x, y))" ..
     1.9  
    1.10  
    1.11  subsection {* Embedded terms *}
    1.12 @@ -42,7 +42,7 @@
    1.13    shows "(!!x. PROP A(x) && PROP B(x)) == ((!!x. PROP A(x)) && (!!x. PROP B(x)))"
    1.14  proof
    1.15    assume conj: "!!x. PROP A(x) && PROP B(x)"
    1.16 -  show "(\<And>x. PROP A(x)) && (\<And>x. PROP B(x))"
    1.17 +  show "(!!x. PROP A(x)) && (!!x. PROP B(x))"
    1.18    proof -
    1.19      fix x
    1.20      from conj show "PROP A(x)" by (rule conjunctionD1)