--- 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);
--- 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"
--- 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"
--- 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);
--- 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();
--- 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;