src/HOL/HOL.ML
changeset 5185 d1067e2c3f9f
parent 5154 40fd46f3d3a1
child 5228 66925577cefe
     1.1 --- a/src/HOL/HOL.ML	Fri Jul 24 13:19:38 1998 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Jul 24 13:27:23 1998 +0200
     1.3 @@ -250,6 +250,12 @@
     1.4   (fn major::prems =>
     1.5    [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
     1.6  
     1.7 +Goal "?! x. P x ==> ? x. P x";
     1.8 +be ex1E 1;
     1.9 +br exI 1;
    1.10 +ba 1;
    1.11 +qed "ex1_implies_ex";
    1.12 +
    1.13  
    1.14  (** Select: Hilbert's Epsilon-operator **)
    1.15  section "@";