1.1 --- a/src/HOL/HOL_lemmas.ML	Sun Oct 08 19:58:26 2000 +0200
     1.2 +++ b/src/HOL/HOL_lemmas.ML	Mon Oct 09 09:33:45 2000 +0200
     1.3 @@ -353,14 +353,14 @@
     1.4  
     1.5  (*Easier to apply than someI: conclusion has only one occurrence of P*)
     1.6  val prems = Goal
     1.7 -    "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)";
     1.8 +    "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
     1.9  by (resolve_tac prems 1);
    1.10  by (rtac someI 1);
    1.11  by (resolve_tac prems 1) ;
    1.12  qed "someI2";
    1.13  
    1.14  (*Easier to apply than someI2 if witness ?a comes from an EX-formula*)
    1.15 -val [major,minor] = Goal "[| EX a. P a;  !!x. P x ==> Q x |] ==> Q (Eps P)";
    1.16 +val [major,minor] = Goal "[| EX a. P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
    1.17  by (rtac (major RS exE) 1);
    1.18  by (etac someI2 1 THEN etac minor 1);
    1.19  qed "someI2_ex";