isatool expandshort;
authorwenzelm
Fri Jul 31 11:03:31 1998 +0200 (1998-07-31)
changeset 522866925577cefe
parent 5227 e5a6ace920a0
child 5229 7c8abffc4413
isatool expandshort;
src/HOL/HOL.ML
     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