src/HOL/cladata.ML
changeset 3842 b55686a7b22c
parent 3615 e5322197cfea
child 4059 59c1422c9da5
     1.1 --- a/src/HOL/cladata.ML	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/cladata.ML	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  
     1.5  (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
     1.6  qed_goal "alt_ex1E" thy
     1.7 -    "[| ?! x.P(x);                                              \
     1.8 +    "[| ?! x. P(x);                                              \
     1.9  \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
    1.10  \    |] ==> R"
    1.11   (fn major::prems =>