src/HOL/HOL.ML
changeset 5228 66925577cefe
parent 5185 d1067e2c3f9f
child 5299 d15a4155b96b
     1.1 --- a/src/HOL/HOL.ML	Fri Jul 31 11:03:21 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Jul 31 11:03:31 1998 +0200
     1.3 @@ -251,9 +251,9 @@
     1.4    [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
     1.5  
     1.6  Goal "?! x. P x ==> ? x. P x";
     1.7 -be ex1E 1;
     1.8 -br exI 1;
     1.9 -ba 1;
    1.10 +by (etac ex1E 1);
    1.11 +by (rtac exI 1);
    1.12 +by (assume_tac 1);
    1.13  qed "ex1_implies_ex";
    1.14  
    1.15