1.1 --- a/src/HOL/HOL_lemmas.ML	Wed Jan 31 01:13:01 2001 +0100
     1.2 +++ b/src/HOL/HOL_lemmas.ML	Wed Jan 31 10:13:22 2001 +0100
     1.3 @@ -346,34 +346,30 @@
     1.4  qed "someI_ex";
     1.5  
     1.6  (*Easier to apply than someI: conclusion has only one occurrence of P*)
     1.7 -val prems = Goal
     1.8 -    "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
     1.9 +val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
    1.10  by (resolve_tac prems 1);
    1.11  by (rtac someI 1);
    1.12  by (resolve_tac prems 1) ;
    1.13  qed "someI2";
    1.14  
    1.15  (*Easier to apply than someI2 if witness ?a comes from an EX-formula*)
    1.16 -val [major,minor] = Goal "[| EX a. P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
    1.17 +val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
    1.18  by (rtac (major RS exE) 1);
    1.19  by (etac someI2 1 THEN etac minor 1);
    1.20  qed "someI2_ex";
    1.21  
    1.22 -val prems = Goal
    1.23 -    "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a";
    1.24 +val prems = Goal "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a";
    1.25  by (rtac someI2 1);
    1.26  by (REPEAT (ares_tac prems 1)) ;
    1.27  qed "some_equality";
    1.28  
    1.29 -Goalw [Ex1_def] "[| EX!x. P x; P a |] ==> (SOME x. P x) = a";
    1.30 +Goal "[| EX!x. P x; P a |] ==> (SOME x. P x) = a";
    1.31  by (rtac some_equality 1);
    1.32 -by (atac 1);
    1.33 -by (etac exE 1);
    1.34 -by (etac conjE 1);
    1.35 -by (rtac allE 1);
    1.36 -by (atac 1);
    1.37 -by (etac impE 1);
    1.38 -by (atac 1);
    1.39 +by  (atac 1);
    1.40 +by (etac ex1E 1);
    1.41 +by (etac all_dupE 1);
    1.42 +by (dtac mp 1);
    1.43 +by  (atac 1);
    1.44  by (etac ssubst 1);
    1.45  by (etac allE 1);
    1.46  by (etac mp 1);
    1.47 @@ -485,3 +481,4 @@
    1.48  
    1.49  
    1.50  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
    1.51 +