prefer plain ASCII here;
authorwenzelm
Mon Apr 07 21:29:46 2008 +0200 (2008-04-07 ago)
changeset 265729178a7f4c4c8
parent 26571 114da911bc41
child 26573 ea36563210cc
prefer plain ASCII here;
src/Pure/Pure.thy
     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)