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