tuned;
authorwenzelm
Fri Jul 20 21:53:27 2001 +0200 (2001-07-20)
changeset 11433cf7dae62d69d
parent 11432 8a203ae6efe3
child 11434 996bd4eb0ef3
tuned;
src/HOL/HOL_lemmas.ML
     1.1 --- a/src/HOL/HOL_lemmas.ML	Fri Jul 20 21:52:54 2001 +0200
     1.2 +++ b/src/HOL/HOL_lemmas.ML	Fri Jul 20 21:53:27 2001 +0200
     1.3 @@ -421,7 +421,7 @@
     1.4  by (REPEAT (ares_tac [prema,premx] 1));
     1.5  qed "theI";
     1.6  
     1.7 -Goal "(EX! x. P x) ==> P (THE x. P x)";
     1.8 +Goal "EX! x. P x ==> P (THE x. P x)";
     1.9  by (etac ex1E 1);
    1.10  by (etac theI 1);
    1.11  by (etac allE 1);