# 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";