# HG changeset patch # User nipkow # Date 971076825 -7200 # Node ID dfff821d2949705e0a21a4cda835ffeb7e16a575 # Parent dd25f5f9641af64818a8cb5e011528efff4c817f @ -> SOME diff -r dd25f5f9641a -r dfff821d2949 src/HOL/HOL_lemmas.ML --- a/src/HOL/HOL_lemmas.ML Sun Oct 08 19:58:26 2000 +0200 +++ b/src/HOL/HOL_lemmas.ML Mon Oct 09 09:33:45 2000 +0200 @@ -353,14 +353,14 @@ (*Easier to apply than someI: conclusion has only one occurrence of P*) val prems = Goal - "[| P a; !!x. P x ==> Q x |] ==> Q (@x. P x)"; + "[| P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"; by (resolve_tac prems 1); by (rtac someI 1); by (resolve_tac prems 1) ; qed "someI2"; (*Easier to apply than someI2 if witness ?a comes from an EX-formula*) -val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"; +val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"; by (rtac (major RS exE) 1); by (etac someI2 1 THEN etac minor 1); qed "someI2_ex";