# HG changeset patch
# User nipkow
# Date 971093455 -7200
# Node ID 76646fc8b1bfe1f5353e43e4dd0e3104e69d0f4c
# Parent  ba7955d211c40a0e301caf352e0e541fb70e971e
ex_someI -> someI_ex

diff -r ba7955d211c4 -r 76646fc8b1bf src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Mon Oct 09 14:10:55 2000 +0200
@@ -349,7 +349,7 @@
 Goal "EX x. P x ==> P (SOME x. P x)";
 by (etac exE 1);
 by (etac someI 1);
-qed "ex_someI";
+qed "someI_ex";
 
 (*Easier to apply than someI: conclusion has only one occurrence of P*)
 val prems = Goal
@@ -366,12 +366,12 @@
 qed "someI2_ex";
 
 val prems = Goal
-    "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";
+    "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a";
 by (rtac someI2 1);
 by (REPEAT (ares_tac prems 1)) ;
 qed "some_equality";
 
-Goalw [Ex1_def] "[| EX!x. P x; P a |] ==> (@x. P x) = a";
+Goalw [Ex1_def] "[| EX!x. P x; P a |] ==> (SOME x. P x) = a";
 by (rtac some_equality 1);
 by (atac 1);
 by (etac exE 1);
@@ -386,20 +386,20 @@
 by (atac 1);
 qed "some1_equality";
 
-Goal "P (@ x. P x) =  (EX x. P x)";
+Goal "P (SOME x. P x) =  (EX x. P x)";
 by (rtac iffI 1);
 by (etac exI 1);
 by (etac exE 1);
 by (etac someI 1);
 qed "some_eq_ex";
 
-Goal "(@y. y=x) = x";
+Goal "(SOME y. y=x) = x";
 by (rtac some_equality 1);
 by (rtac refl 1);
 by (atac 1);
 qed "some_eq_trivial";
 
-Goal "(@y. x=y) = x";
+Goal "(SOME y. x=y) = x";
 by (rtac some_equality 1);
 by (rtac refl 1);
 by (etac sym 1);
diff -r ba7955d211c4 -r 76646fc8b1bf src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 09 14:10:55 2000 +0200
@@ -81,7 +81,7 @@
 lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
 proof (unfold Meet_def)
   from ex_Inf show "is_Inf A (SOME inf. is_Inf A inf)"
-    by (rule ex_someI)
+    by (rule someI_ex)
 qed
 
 lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
@@ -94,7 +94,7 @@
 lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
 proof (unfold Join_def)
   from ex_Sup show "is_Sup A (SOME sup. is_Sup A sup)"
-    by (rule ex_someI)
+    by (rule someI_ex)
 qed
 
 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
diff -r ba7955d211c4 -r 76646fc8b1bf src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Mon Oct 09 14:10:55 2000 +0200
@@ -70,7 +70,7 @@
 lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
 proof (unfold meet_def)
   from ex_inf show "is_inf x y (SOME inf. is_inf x y inf)"
-    by (rule ex_someI)
+    by (rule someI_ex)
 qed
 
 lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
@@ -86,7 +86,7 @@
 lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
 proof (unfold join_def)
   from ex_sup show "is_sup x y (SOME sup. is_sup x y sup)"
-    by (rule ex_someI)
+    by (rule someI_ex)
 qed
 
 lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
diff -r ba7955d211c4 -r 76646fc8b1bf src/HOL/NumberTheory/Chinese.ML
--- a/src/HOL/NumberTheory/Chinese.ML	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/NumberTheory/Chinese.ML	Mon Oct 09 14:10:55 2000 +0200
@@ -210,7 +210,7 @@
 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
 by (rewtac xilin_sol_def);
 by (Asm_simp_tac 7);
-by (rtac (ex1_implies_ex RS ex_someI) 7);
+by (rtac (ex1_implies_ex RS someI_ex) 7);
 by (rtac unique_xi_sol 7);
 by (rtac funprod_zdvd 4);
 by (rewtac m_cond_def);
diff -r ba7955d211c4 -r 76646fc8b1bf src/HOL/NumberTheory/EulerFermat.ML
--- a/src/HOL/NumberTheory/EulerFermat.ML	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.ML	Mon Oct 09 14:10:55 2000 +0200
@@ -152,7 +152,7 @@
 Goal "[| #1<m; is_RRset A m; a:A |] \
 \     ==> zcong a (@ b. [a = b](mod m) & b : norRRset m) m & \
 \         (@ b. [a = b](mod m) & b : norRRset m) : norRRset m";
-by (rtac (norR_mem_unique RS ex1_implies_ex RS ex_someI) 1);
+by (rtac (norR_mem_unique RS ex1_implies_ex RS someI_ex) 1);
 by (rtac RRset_gcd 2);
 by (ALLGOALS Asm_simp_tac);
 val lemma_some = result();
diff -r ba7955d211c4 -r 76646fc8b1bf src/HOL/NumberTheory/WilsonBij.ML
--- a/src/HOL/NumberTheory/WilsonBij.ML	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.ML	Mon Oct 09 14:10:55 2000 +0200
@@ -15,7 +15,7 @@
       "[| p:zprime; #0<a; a<p |] \ 
 \     ==> #0 <= (inv p a) & (inv p a)<p & [a*(inv p a) = #1](mod p)";
 by (Asm_simp_tac 1);
-by (rtac (zcong_lineq_unique RS ex1_implies_ex RS ex_someI) 1);
+by (rtac (zcong_lineq_unique RS ex1_implies_ex RS someI_ex) 1);
 by (etac zless_zprime_imp_zrelprime 2);
 by (rewtac zprime_def);
 by Auto_tac;