# HG changeset patch # User berghofe # Date 901279643 -7200 # Node ID d1067e2c3f9f1f9bcdf9c1e3b6497cd51cc67ca7 # Parent 9b8547a9496afa9c74bd507626d698437c36684e Added theorem ex1_implies_ex. diff -r 9b8547a9496a -r d1067e2c3f9f src/HOL/HOL.ML --- 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 "@";