# HG changeset patch
# User paulson
# Date 969024650 -7200
# Node ID dfe4747c8318110f715b9489f38747d74c24e936
# Parent  4753185f1dd24ddbf405a94647388b56814b49cb
the final renaming: selectI -> someI

diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Algebra/abstract/Ring.ML
--- a/src/HOL/Algebra/abstract/Ring.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -288,7 +288,7 @@
   "!! a::'a::ring. a dvd <1> ==> a * inverse a = <1>";
 by (Asm_simp_tac 1);
 by (Clarify_tac 1);
-by (rtac selectI 1);
+by (rtac someI 1);
 by (rtac sym 1);
 by (assume_tac 1);
 qed "r_inverse_ring";
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Auth/Public.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -142,7 +142,7 @@
 
 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
 by (rtac (lemma RS exE) 1);
-by (rtac selectI 1);
+by (rtac someI 1);
 by (Fast_tac 1);
 qed "Nonce_supply";
 
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Auth/Shared.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -158,7 +158,7 @@
 
 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
 by (rtac (lemma RS exE) 1);
-by (rtac selectI 1);
+by (rtac someI 1);
 by (Blast_tac 1);
 qed "Nonce_supply";
 
@@ -192,7 +192,7 @@
 
 Goal "Key (@ K. Key K ~: used evs) ~: used evs";
 by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
-by (rtac selectI 1);
+by (rtac someI 1);
 by (Blast_tac 1);
 qed "Key_supply";
 
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/BCV/Kildall.ML
--- a/src/HOL/BCV/Kildall.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/BCV/Kildall.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -185,7 +185,7 @@
 by(asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
 by(clarify_tac (claset() delrules [disjCI]) 1);
 by(subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [selectI]) 2);
+ by (fast_tac (claset() addIs [someI]) 2);
 by(subgoal_tac "ss : list (size ss) A" 1);
  by (blast_tac (claset() addSIs [listI]) 2);
 by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
@@ -213,7 +213,7 @@
  by(rotate_tac ~1 1);
  by(asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
 by(subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [selectI]) 2);
+ by (fast_tac (claset() addIs [someI]) 2);
 by (blast_tac (claset() addDs [boundedD]) 1);
 qed "iter_induct";
 
@@ -230,7 +230,7 @@
 br impI 1;
 by(stac decomp_propa 1);
  by(subgoal_tac "(@p. p:w) : w" 1);
-  by (fast_tac (claset() addIs [selectI]) 2);
+  by (fast_tac (claset() addIs [someI]) 2);
  by (blast_tac (claset() addDs [boundedD]) 1);
 by (Simp_tac 1);
 qed "iter_unfold";
@@ -306,7 +306,7 @@
 be impE 1;
  by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
 by(subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [selectI]) 2);
+ by (fast_tac (claset() addIs [someI]) 2);
 by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
  by (blast_tac (claset() addIs [pres_typeD,listE_nth_in]) 2);
 be impE 1;
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/Fun.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -24,7 +24,7 @@
 (*"choice" is now proved in Tools/meson.ML*)
 
 Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
-by (fast_tac (claset() addEs [selectI]) 1);
+by (fast_tac (claset() addEs [someI]) 1);
 qed "bchoice";
 
 
@@ -115,7 +115,7 @@
 
 Goal "inj(f) ==> (@x. f(x)=f(y)) = y";
 by (etac injD 1);
-by (rtac selectI 1);
+by (rtac someI 1);
 by (rtac refl 1);
 qed "inj_select";
 
@@ -212,7 +212,7 @@
 qed "comp_inj_on";
 
 Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
-by (fast_tac (claset() addIs [selectI]) 1);
+by (fast_tac (claset() addIs [someI]) 1);
 qed "f_inv_f";
 
 Goal "surj f ==> f(inv f y) = y";
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/HOL.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -9,7 +9,7 @@
   val refl = refl;
   val subst = subst;
   val ext = ext;
-  val selectI = selectI;
+  val someI = someI;
   val impI = impI;
   val mp = mp;
   val True_def = True_def;
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/HOL.thy	Fri Sep 15 15:30:50 2000 +0200
@@ -159,7 +159,7 @@
     rule, and similar to the ABS rule of HOL.*)
   ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
 
-  selectI:      "P (x::'a) ==> P (@x. P x)"
+  someI:        "P (x::'a) ==> P (@x. P x)"
 
   impI:         "(P ==> Q) ==> P-->Q"
   mp:           "[| P-->Q;  P |] ==> Q"
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -16,7 +16,7 @@
 val refl = thm "refl";
 val subst = thm "subst";
 val ext = thm "ext";
-val selectI = thm "selectI";
+val someI = thm "someI";
 val impI = thm "impI";
 val mp = thm "mp";
 val True_def = thm "True_def";
@@ -221,7 +221,7 @@
 section "EX ";
 
 Goalw [Ex_def] "P x ==> EX x::'a. P x";
-by (etac selectI 1) ;
+by (etac someI 1) ;
 qed "exI";
 
 val [major,minor] =
@@ -355,17 +355,17 @@
 (** Select: Hilbert's Epsilon-operator **)
 section "@";
 
-(*Easier to apply than selectI if witness ?a comes from an EX-formula*)
+(*Easier to apply than someI if witness ?a comes from an EX-formula*)
 Goal "EX x. P x ==> P (SOME x. P x)";
 by (etac exE 1);
-by (etac selectI 1);
+by (etac someI 1);
 qed "ex_someI";
 
-(*Easier to apply than selectI: conclusion has only one occurrence of P*)
+(*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)";
 by (resolve_tac prems 1);
-by (rtac selectI 1);
+by (rtac someI 1);
 by (resolve_tac prems 1) ;
 qed "someI2";
 
@@ -400,7 +400,7 @@
 by (rtac iffI 1);
 by (etac exI 1);
 by (etac exE 1);
-by (etac selectI 1);
+by (etac someI 1);
 qed "some_eq_ex";
 
 Goal "(@y. y=x) = x";
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Fri Sep 15 15:30:50 2000 +0200
@@ -332,7 +332,7 @@
                  (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
           by - (drule bspec, assumption, 
                 clarsimp dest!: wtl_method_correct,
-                clarsimp intro!: selectI simp add: unique_epsilon) 
+                clarsimp intro!: someI simp add: unique_epsilon) 
       qed
     qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
   qed
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/MicroJava/J/State.ML
--- a/src/HOL/MicroJava/J/State.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/MicroJava/J/State.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -12,7 +12,7 @@
 val new_AddrD = prove_goalw thy [new_Addr_def] 
 "\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
 	asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
-	rtac selectI 1,
+	rtac someI 1,
 	rtac disjI2 1,
 	res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
 	 Auto_tac ]);
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/WF.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -290,7 +290,7 @@
 
 Goalw [the_recfun_def]
     "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)";
-by (eres_inst_tac [("P", "is_recfun r H a")] selectI 1);
+by (eres_inst_tac [("P", "is_recfun r H a")] someI 1);
 qed "is_the_recfun";
 
 Goal "[| wf(r);  trans(r) |] ==> is_recfun r H a (the_recfun r H a)";
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOL/meson_lemmas.ML
--- a/src/HOL/meson_lemmas.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/meson_lemmas.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -9,7 +9,7 @@
 (* "Axiom" of Choice, proved using the description operator *)
 
 Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
-by (fast_tac (claset() addEs [selectI]) 1);
+by (fast_tac (claset() addEs [someI]) 1);
 qed "choice";
 
 
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -68,7 +68,7 @@
 by (subgoal_tac "? ex. move A ex (f s) a (f t)" 1);
 by (Asm_full_simp_tac 2);
 by (etac exE 1);
-by (rtac selectI 1);
+by (rtac someI 1);
 by (assume_tac 1);
 qed"move_is_move";
 
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -86,11 +86,11 @@
 (* Go on as usual *)
 by (etac exE 1);
 by (dres_inst_tac [("x","t'"),
-         ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
+         ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] someI 1);
 by (etac exE 1);
 by (etac conjE 1);
 by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
-by (res_inst_tac [("x","ex")] selectI 1);
+by (res_inst_tac [("x","ex")] someI 1);
 by (etac conjE 1);
 by (assume_tac 1);
 qed"move_is_move_sim";
diff -r 4753185f1dd2 -r dfe4747c8318 src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOLCF/Porder.ML	Fri Sep 15 15:30:50 2000 +0200
@@ -56,7 +56,7 @@
 Goal "M <<| l ==> lub(M) = l";
 by (rtac unique_lub 1);
 by (stac lub 1);
-by (etac selectI 1);
+by (etac someI 1);
 by (atac 1);
 qed "thelubI";
 
@@ -130,7 +130,7 @@
 Goalw [finite_chain_def]
         "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
 by (rtac lub_finch1 1);
-by (best_tac (claset() addIs [selectI]) 2);
+by (best_tac (claset() addIs [someI]) 2);
 by (Blast_tac 1);
 qed "lub_finch2";