src/HOL/HOL.ML
changeset 5228 66925577cefe
parent 5185 d1067e2c3f9f
child 5299 d15a4155b96b
equal deleted inserted replaced
5227:e5a6ace920a0 5228:66925577cefe
   249     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
   249     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
   250  (fn major::prems =>
   250  (fn major::prems =>
   251   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
   251   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
   252 
   252 
   253 Goal "?! x. P x ==> ? x. P x";
   253 Goal "?! x. P x ==> ? x. P x";
   254 be ex1E 1;
   254 by (etac ex1E 1);
   255 br exI 1;
   255 by (rtac exI 1);
   256 ba 1;
   256 by (assume_tac 1);
   257 qed "ex1_implies_ex";
   257 qed "ex1_implies_ex";
   258 
   258 
   259 
   259 
   260 (** Select: Hilbert's Epsilon-operator **)
   260 (** Select: Hilbert's Epsilon-operator **)
   261 section "@";
   261 section "@";