# HG changeset patch
# User paulson
# Date 969014397 -7200
# Node ID 4753185f1dd24ddbf405a94647388b56814b49cb
# Parent  264b16d934f983660c46460ef3294c23852824af
renamed (most of...) the select rules

diff -r 264b16d934f9 -r 4753185f1dd2 doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Fri Sep 15 11:34:46 2000 +0200
+++ b/doc-src/HOL/HOL.tex	Fri Sep 15 12:39:57 2000 +0200
@@ -290,7 +290,7 @@
 \tdx{impI}          (P ==> Q) ==> P-->Q
 \tdx{mp}            [| P-->Q;  P |] ==> Q
 \tdx{iff}           (P-->Q) --> (Q-->P) --> (P=Q)
-\tdx{selectI}       P(x::'a) ==> P(@x. P x)
+\tdx{someI}         P(x::'a) ==> P(@x. P x)
 \tdx{True_or_False} (P=True) | (P=False)
 \end{ttbox}
 \caption{The \texttt{HOL} rules} \label{hol-rules}
@@ -302,9 +302,9 @@
 \item[\tdx{ext}] expresses extensionality of functions.
 \item[\tdx{iff}] asserts that logically equivalent formulae are
   equal.
-\item[\tdx{selectI}] gives the defining property of the Hilbert
+\item[\tdx{someI}] gives the defining property of the Hilbert
   $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
-  \tdx{select_equality} (see below) is often easier to use.
+  \tdx{some_equality} (see below) is often easier to use.
 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
     fact, the $\varepsilon$-operator already makes the logic classical, as
     shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
@@ -409,7 +409,7 @@
 \tdx{ex1E}      [| ?! x. P x;  !!x. [| P x;  ! y. P y --> y=x |] ==> R 
           |] ==> R
 
-\tdx{select_equality} [| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a
+\tdx{some_equality}   [| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a
 \subcaption{Quantifiers and descriptions}
 
 \tdx{ccontr}          (~P ==> False) ==> P
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/AxClasses/Lattice/CLattice.ML
--- a/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -51,14 +51,14 @@
 
 val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
   by (cut_facts_tac prems 1);
-  by (rtac selectI2 1);
+  by (rtac someI2 1);
   by (rtac Inf_is_Inf 1);
   by (rewtac is_Inf_def);
   by (Fast_tac 1);
 qed "Inf_lb";
 
 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
-  by (rtac selectI2 1);
+  by (rtac someI2 1);
   by (rtac Inf_is_Inf 1);
   by (rewtac is_Inf_def);
   by (Step_tac 1);
@@ -71,14 +71,14 @@
 
 val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
   by (cut_facts_tac prems 1);
-  by (rtac selectI2 1);
+  by (rtac someI2 1);
   by (rtac Sup_is_Sup 1);
   by (rewtac is_Sup_def);
   by (Fast_tac 1);
 qed "Sup_ub";
 
 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
-  by (rtac selectI2 1);
+  by (rtac someI2 1);
   by (rtac Sup_is_Sup 1);
   by (rewtac is_Sup_def);
   by (Step_tac 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/BCV/Semilat.ML
--- a/src/HOL/BCV/Semilat.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/BCV/Semilat.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -162,7 +162,7 @@
 
 Goalw [some_lub_def,is_lub_def]
  "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u";
-br selectI2 1;
+br someI2 1;
  ba 1;
 by(blast_tac (claset() addIs [antisymD]
                        addSDs [acyclic_impl_antisym_rtrancl]) 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Finite.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -323,7 +323,7 @@
 Goalw [card_def]
      "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)";
 by (asm_simp_tac (simpset() addsimps [lemma]) 1);
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (auto_tac (claset() addIs [finite_imp_cardR],
 	      simpset() addcongs [conj_cong]
 		        addsimps [symmetric card_def,
@@ -596,7 +596,7 @@
 Goalw [fold_def]
      "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
 by (asm_simp_tac (simpset() addsimps [lemma]) 1);
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (auto_tac (claset() addIs [finite_imp_foldSet],
 	      simpset() addcongs [conj_cong]
 		        addsimps [symmetric fold_def,
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Fun.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -584,7 +584,7 @@
 
 Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
 \                ==> (lam x: B. (Inv A f) x) : B funcset A";
-by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
+by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
 qed "Inv_funcset";
 
 
@@ -592,14 +592,14 @@
 \     ==> (lam y: B. (Inv A f) y) (f x) = x";
 by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by Auto_tac;
 qed "Inv_f_f";
 
 Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
 \     ==> f ((lam y: B. (Inv A f y)) x) = x";
 by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
-by (fast_tac (claset() addIs [selectI2]) 1);
+by (fast_tac (claset() addIs [someI2]) 1);
 qed "f_Inv_f";
 
 Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -49,7 +49,7 @@
 by (etac subst 1 THEN assume_tac 1);
 qed "trans";
 
-val prems = goal (the_context ()) "(A == B) ==> A = B";
+val prems = goal (the_context()) "(A == B) ==> A = B";
 by (rewrite_goals_tac prems);
 by (rtac refl 1);
 qed "def_imp_eq";
@@ -140,11 +140,11 @@
 by (etac fun_cong 1);
 qed "spec";
 
-val major::prems= goal (the_context ()) "[| ALL x. P(x);  P(x) ==> R |] ==> R";
+val major::prems = Goal "[| ALL x. P(x);  P(x) ==> R |] ==> R";
 by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
 qed "allE";
 
-val prems = goal (the_context ())
+val prems = Goal
     "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
 by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
 qed "all_dupE";
@@ -356,7 +356,7 @@
 section "@";
 
 (*Easier to apply than selectI if witness ?a comes from an EX-formula*)
-Goal "EX a. P a ==> P (SOME x. P x)";
+Goal "EX x. P x ==> P (SOME x. P x)";
 by (etac exE 1);
 by (etac selectI 1);
 qed "ex_someI";
@@ -367,22 +367,22 @@
 by (resolve_tac prems 1);
 by (rtac selectI 1);
 by (resolve_tac prems 1) ;
-qed "selectI2";
+qed "someI2";
 
-(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
+(*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)";
 by (rtac (major RS exE) 1);
-by (etac selectI2 1 THEN etac minor 1);
-qed "selectI2EX";
+by (etac someI2 1 THEN etac minor 1);
+qed "someI2EX";
 
 val prems = Goal
     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (REPEAT (ares_tac prems 1)) ;
-qed "select_equality";
+qed "some_equality";
 
 Goalw [Ex1_def] "[| EX!x. P x; P a |] ==> (@x. P x) = a";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (atac 1);
 by (etac exE 1);
 by (etac conjE 1);
@@ -394,31 +394,31 @@
 by (etac allE 1);
 by (etac mp 1);
 by (atac 1);
-qed "select1_equality";
+qed "some1_equality";
 
 Goal "P (@ x. P x) =  (EX x. P x)";
 by (rtac iffI 1);
 by (etac exI 1);
 by (etac exE 1);
 by (etac selectI 1);
-qed "select_eq_Ex";
+qed "some_eq_ex";
 
 Goal "(@y. y=x) = x";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (rtac refl 1);
 by (atac 1);
-qed "Eps_eq";
+qed "some_eq_trivial";
 
-Goal "(Eps (op = x)) = x";
-by (rtac select_equality 1);
+Goal "(@y. x=y) = x";
+by (rtac some_equality 1);
 by (rtac refl 1);
 by (etac sym 1);
-qed "Eps_sym_eq";
+qed "some_sym_eq_trivial";
 
 (** Classical intro rules for disjunction and existential quantifiers *)
 section "classical intro rules";
 
-val prems= Goal "(~Q ==> P) ==> P|Q";
+val prems = Goal "(~Q ==> P) ==> P|Q";
 by (rtac classical 1);
 by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
 by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -37,7 +37,7 @@
 
 Goalw [gcd_def] "0<n ==> n = gcd n n";
 by (ftac cd_nnn 1);
-by (rtac (select_equality RS sym) 1);
+by (rtac (some_equality RS sym) 1);
 by (blast_tac (claset() addDs [cd_le]) 1);
 by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);
 qed "gcd_nnn";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -281,7 +281,7 @@
 by Auto_tac;
 qed "zmult_0_eq_iff";
 
-Addsimps [zmult_eq_0_iff, zmult_0_eq_iff];
+AddIffs [zmult_eq_0_iff, zmult_0_eq_iff];
 
 Goal "(w < z + (#1::int)) = (w<z | w=z)";
 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -43,10 +43,10 @@
 
 (* To HOL.ML *)
 
-val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" 
+val ex1_some_eq_trivial = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" 
 	(fn prems => [
 	cut_facts_tac prems 1,
-	rtac select_equality 1,
+	rtac some_equality 1,
 	 atac 1,
 	etac ex1E 1,
 	etac all_dupE 1,
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/MicroJava/JVM/Store.ML
--- a/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -6,5 +6,5 @@
 
 Goalw [newref_def]
  "hp x = None \\<longrightarrow> hp (newref hp) = None";
-by (fast_tac (claset() addIs [selectI2EX] addss (simpset())) 1);
+by (fast_tac (claset() addIs [someI2EX] addss (simpset())) 1);
 qed_spec_mp "newref_None";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Nat.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -76,7 +76,7 @@
 
 Goalw [Least_nat_def]
  "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (fold_goals_tac [Least_nat_def]);
 by (safe_tac (claset() addSEs [LeastI]));
 by (rename_tac "j" 1);
@@ -88,7 +88,7 @@
 by (Blast_tac 1);
 by (hyp_subst_tac 1);
 by (rewtac Least_nat_def);
-by (rtac (select_equality RS arg_cong RS sym) 1);
+by (rtac (some_equality RS arg_cong RS sym) 1);
 by (blast_tac (claset() addDs [Suc_mono]) 1);
 by (cut_inst_tac [("m","m")] less_linear 1);
 by (blast_tac (claset() addIs [Suc_mono]) 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/NatDef.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -476,7 +476,7 @@
 
 val [prem1,prem2] = Goalw [Least_nat_def]
     "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (blast_tac (claset() addSIs [prem1,prem2]) 1);
 by (cut_facts_tac [less_linear] 1);
 by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/NumberTheory/IntPrimes.ML
--- a/src/HOL/NumberTheory/IntPrimes.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -569,7 +569,7 @@
 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
 by (subgoal_tac "m*k<m*#1" 1);
 by (dtac (zmult_zless_cancel1 RS iffD1) 1);
-by Auto_tac;  
+by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
 qed "zcong_zless_0";
 
 Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Ord.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -120,10 +120,9 @@
 by (Blast_tac 1);
 qed "linorder_less_linear";
 
-val prems = goal (the_context ())
- "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
-by(cut_facts_tac [linorder_less_linear] 1);
-by(REPEAT(eresolve_tac (prems@[disjE]) 1));
+val prems = Goal "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
+by (cut_facts_tac [linorder_less_linear] 1);
+by (REPEAT(eresolve_tac (prems@[disjE]) 1));
 qed "linorder_less_split";
 
 Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Prod.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -55,10 +55,9 @@
 by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
 qed "ProdI";
 
-val [major] = goalw (the_context ()) [Pair_Rep_def]
-    "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
-by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst),
-            rtac conjI, rtac refl, rtac refl]);
+Goalw [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
+by (dtac (fun_cong RS fun_cong) 1);
+by (Blast_tac 1);
 qed "Pair_Rep_inject";
 
 Goal "inj_on Abs_Prod Prod";
@@ -185,9 +184,8 @@
 qed "Pair_fst_snd_eq";
 
 (*Prevents simplification of c: much faster*)
-val [prem] = goal (the_context ())
-  "p=q ==> split c p = split c q";
-by (rtac (prem RS arg_cong) 1);
+Goal "p=q ==> split c p = split c q";
+by (etac arg_cong 1);
 qed "split_weak_cong";
 
 Goal "(%(x,y). f(x,y)) = f";
@@ -303,7 +301,7 @@
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
 qed "splitE'";
 
-val major::prems = goal (the_context ())
+val major::prems = Goal
     "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
 \    |] ==> R";
 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
@@ -360,7 +358,7 @@
 ### Cannot add premise as rewrite rule because it contains (type) unknowns:
 ### ?y = .x
 Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by ( Simp_tac 1);
 by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
@@ -436,7 +434,7 @@
 by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
 qed "SigmaD2";
 
-val [major,minor]= goal (the_context ())
+val [major,minor]= Goal
     "[| (a,b) : Sigma A B;    \
 \       [| a:A;  b:B(a) |] ==> P   \
 \    |] ==> P";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 12:39:57 2000 +0200
@@ -97,7 +97,7 @@
   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
      ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
 proof (unfold function_norm_def is_function_norm_def 
-  is_continuous_def Sup_def, elim conjE, rule selectI2EX)
+  is_continuous_def Sup_def, elim conjE, rule someI2EX)
   assume "is_normed_vectorspace V norm"
   assume "is_linearform V f" 
   and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/HahnBanach/FunctionOrder.thy
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Sep 15 12:39:57 2000 +0200
@@ -75,11 +75,11 @@
   ==> graph (domain g) (funct g) = g"
 proof (unfold domain_def funct_def graph_def, auto)
   fix a b assume "(a, b) \<in> g"
-  show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule selectI2)
+  show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
   show "\<exists>y. (a, y) \<in> g" ..
   assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
   show "b = (SOME y. (a, y) \<in> g)"
-  proof (rule select_equality [symmetric])
+  proof (rule some_equality [symmetric])
     fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
   qed
 qed
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Sep 15 12:39:57 2000 +0200
@@ -469,7 +469,7 @@
     qed
   qed
   hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
-    by (rule select1_equality) (force!)
+    by (rule some1_equality) (force!)
   thus "h' x = h y + a * xi" by (simp! add: Let_def)
 qed
 
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -43,13 +43,13 @@
 Goalw [FreeUltrafilterNat_def] 
      "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)";
 by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
-by (rtac selectI2 1 THEN ALLGOALS(assume_tac));
+by (rtac someI2 1 THEN ALLGOALS(assume_tac));
 qed "FreeUltrafilterNat_mem";
 Addsimps [FreeUltrafilterNat_mem];
 
 Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat";
 by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
-by (rtac selectI2 1 THEN assume_tac 1);
+by (rtac someI2 1 THEN assume_tac 1);
 by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1);
 qed "FreeUltrafilterNat_finite";
 
@@ -59,7 +59,7 @@
 
 Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat";
 by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
-by (rtac selectI2 1 THEN assume_tac 1);
+by (rtac someI2 1 THEN assume_tac 1);
 by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
 			       Ultrafilter_Filter,Filter_empty_not_mem]) 1);
 qed "FreeUltrafilterNat_empty";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/Hyperreal/Zorn.ML
--- a/src/HOL/Real/Hyperreal/Zorn.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -32,7 +32,7 @@
 by (auto_tac (claset(),simpset() addsimps [super_def,
                maxchain_def,psubset_def]));
 by (rtac swap 1 THEN assume_tac 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (ALLGOALS(Blast_tac));
 qed "Abrial_axiom1";
 
@@ -167,7 +167,7 @@
 Goal "c: chain S - maxchain S ==> \
 \                         (@c'. c': super S c): super S c";
 by (etac (mem_super_Ex RS exE) 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (Auto_tac);
 qed "select_super";
 
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/PRat.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -38,7 +38,7 @@
 by (Fast_tac 1);
 qed "ratrelE_lemma";
 
-val [major,minor] = goal (the_context ())
+val [major,minor] = Goal
   "[| p: ratrel;  \
 \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1*y2 = x2*y1 \
 \                    |] ==> Q |] ==> Q";
@@ -96,7 +96,7 @@
 by (Asm_full_simp_tac 1);
 qed "inj_prat_of_pnat";
 
-val [prem] = goal (the_context ())
+val [prem] = Goal
     "(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [prat_def] Rep_prat RS quotientE) 1);
@@ -611,7 +611,7 @@
 by (simp_tac (simpset() addsimps [prat_le_eq_less_or_eq]) 1);
 qed "prat_le_refl";
 
-val prems = goal (the_context ()) "!!i. [| i <= j; j < k |] ==> i < (k::prat)";
+Goal "[| i <= j; j < k |] ==> i < (k::prat)";
 by (dtac prat_le_imp_less_or_eq 1);
 by (fast_tac (claset() addIs [prat_less_trans]) 1);
 qed "prat_le_less_trans";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/PReal.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -698,7 +698,7 @@
 by (rtac preal_mult_inv 1);
 qed "preal_mult_inv_right";
 
-val [prem] = goal (the_context ())
+val [prem] = Goal
     "(!!u. z = Abs_preal(u) ==> P) ==> P";
 by (cut_inst_tac [("x1","z")] 
     (rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1);
@@ -779,12 +779,12 @@
 by (Simp_tac 1);
 qed "preal_le_refl";
 
-val prems = goal (the_context ()) "!!i. [| i <= j; j < k |] ==> i < (k::preal)";
+Goal "[| i <= j; j < k |] ==> i < (k::preal)";
 by (dtac preal_le_imp_less_or_eq 1);
 by (fast_tac (claset() addIs [preal_less_trans]) 1);
 qed "preal_le_less_trans";
 
-val prems = goal (the_context ()) "!!i. [| i < j; j <= k |] ==> i < (k::preal)";
+Goal "[| i < j; j <= k |] ==> i < (k::preal)";
 by (dtac preal_le_imp_less_or_eq 1);
 by (fast_tac (claset() addIs [preal_less_trans]) 1);
 qed "preal_less_le_trans";
@@ -804,7 +804,7 @@
 by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
 qed "not_less_not_eq_preal_less";
 
-(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
+(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
 
 (**** Set up all lemmas for proving A < B ==> ?D. A + D = B ****)
 (**** Gleason prop. 9-3.5(iv) p. 123 ****)
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/RealDef.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -35,7 +35,7 @@
 by (Blast_tac 1);
 qed "realrelE_lemma";
 
-val [major,minor] = goal (the_context ())
+val [major,minor] = Goal
   "[| p: realrel;  \
 \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1 \
 \                    |] ==> Q |] ==> Q";
@@ -94,7 +94,7 @@
 by (Asm_full_simp_tac 1);
 qed "inj_real_of_preal";
 
-val [prem] = goal (the_context ())
+val [prem] = Goal
     "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
 by (res_inst_tac [("x1","z")] 
     (rewrite_rule [real_def] Rep_real RS quotientE) 1);
@@ -500,7 +500,7 @@
 Goalw [rinv_def] "x ~= 0 ==> rinv(x)*x = 1r";
 by (ftac real_mult_inv_left_ex 1);
 by (Step_tac 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by Auto_tac;
 qed "real_mult_inv_left";
 
@@ -533,7 +533,7 @@
 Goalw [rinv_def] "x ~= 0 ==> rinv(x) ~= 0";
 by (ftac real_mult_inv_left_ex 1);
 by (etac exE 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [real_mult_0,
     real_zero_not_eq_one]));
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Relation.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -442,12 +442,12 @@
 by (rtac CollectI 1);
 by (rtac allI 1);
 by (etac allE 1);
-by (rtac (select_eq_Ex RS iffD2) 1);
+by (rtac (some_eq_ex RS iffD2) 1);
 by (etac ex1_implies_ex 1);
 by (rtac ext 1);
 by (etac CollectE 1);
 by (REPEAT (etac allE 1));
-by (rtac (select1_equality RS sym) 1);
+by (rtac (some1_equality RS sym) 1);
 by (atac 1);
 by (atac 1);
 qed "fun_rel_comp_unique";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Set.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -720,13 +720,11 @@
 
 (*Split ifs on either side of the membership relation.
 	Not for Addsimps -- can cause goals to blow up!*)
-bind_thm ("split_if_mem1", 
-    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. x : ?b")] split_if);
-bind_thm ("split_if_mem2", 
-    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. ?a : x")] split_if);
+bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
+bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
 
 bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
-		  split_if_mem1, split_if_mem2]);
+			 split_if_mem1, split_if_mem2]);
 
 
 (*Each of these has ALREADY been added to simpset() above.*)
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -245,7 +245,7 @@
       end;
 
     val rec_total_thms = map (fn r =>
-      r RS ex1_implies_ex RS (select_eq_Ex RS iffD2)) rec_unique_thms;
+      r RS ex1_implies_ex RS (some_eq_ex RS iffD2)) rec_unique_thms;
 
     (* define primrec combinators *)
 
@@ -276,7 +276,7 @@
 
     val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
       (cterm_of (Theory.sign_of thy2) t) (fn _ =>
-        [rtac select1_equality 1,
+        [rtac some1_equality 1,
          resolve_tac rec_unique_thms 1,
          resolve_tac rec_intrs 1,
          rewrite_goals_tac [o_def, fun_rel_comp_def],
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -193,7 +193,7 @@
 (* typedef_proof interface *)
 
 fun typedef_attribute cset do_typedef (thy, thm) =
-  (check_nonempty cset (thm RS (select_eq_Ex RS iffD2)); (thy |> do_typedef, thm));
+  (check_nonempty cset (thm RS (some_eq_ex RS iffD2)); (thy |> do_typedef, thm));
 
 fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
   let
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Trancl.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -254,7 +254,7 @@
 qed "trancl_induct";
 
 (*Another induction rule for trancl, incorporating transitivity.*)
-val major::prems = goal (the_context ())
+val major::prems = Goal
  "[| (x,y) : r^+; \
 \    !!x y. (x,y) : r ==> P x y; \
 \    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -88,7 +88,7 @@
 val [surj,prem] = Goalw [inv_def]
      "[| surj h;  !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z";
 by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (dres_inst_tac [("f", "g")] arg_cong 2);
 by (auto_tac (claset(), simpset() addsimps [prem]));
 qed "fst_inv_equalityI";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Univ.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -387,12 +387,8 @@
 by (Blast_tac 1);
 qed "Funs_mono";
 
-val [p] = goalw (the_context ()) [Funs_def] "(!!x. f x : S) ==> f : Funs S";
-by (rtac CollectI 1);
-by (rtac subsetI 1);
-by (etac rangeE 1);
-by (etac ssubst 1);
-by (rtac p 1);
+val [prem] = Goalw [Funs_def] "(!!x. f x : S) ==> f : Funs S";
+by (blast_tac (claset() addIs [prem]) 1);
 qed "FunsI";
 
 Goalw [Funs_def] "f : Funs S ==> f x : S";
@@ -401,8 +397,8 @@
 by (rtac rangeI 1);
 qed "FunsD";
 
-val [p1, p2] = goalw (the_context ()) [o_def]
-  "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
+val [p1, p2] = Goalw [o_def]
+   "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
 by (rtac (p2 RS ext) 1);
 by (rtac (p1 RS FunsD) 1);
 qed "Funs_inv";
@@ -412,7 +408,7 @@
 by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1);
 by (rtac ext 1);
 by (rtac (p1 RS FunsD RS rangeE) 1);
-by (etac (exI RS (select_eq_Ex RS iffD2)) 1);
+by (etac (exI RS (some_eq_ex RS iffD2)) 1);
 qed "Funs_rangeE";
 
 Goal "a : S ==> (%x. a) : Funs S";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Vimage.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -77,11 +77,9 @@
 Addsimps [vimage_Collect_eq];
 
 (*A strange result used in Tools/inductive_package*)
-bind_thm ("vimage_Collect", 
-	  allI RS 
-	  prove_goalw (the_context ()) [vimage_def]
-	  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
-	      (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
+val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
+by (force_tac (claset(), simpset() addsimps prems) 1);
+qed "vimage_Collect";
 
 Addsimps [vimage_empty, vimage_Un, vimage_Int];
 
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/WF_Rel.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -150,14 +150,14 @@
  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
  by (rtac allI 1);
  by (Simp_tac 1);
- by (rtac selectI2EX 1);
+ by (rtac someI2EX 1);
   by (Blast_tac 1);
  by (Blast_tac 1);
 by (rtac allI 1);
 by (induct_tac "n" 1);
  by (Asm_simp_tac 1);
 by (Simp_tac 1);
-by (rtac selectI2EX 1);
+by (rtac someI2EX 1);
  by (Blast_tac 1);
 by (Blast_tac 1);
 qed "wf_iff_no_infinite_down_chain";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/cladata.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -59,7 +59,7 @@
                        addSEs [conjE,disjE,impCE,FalseE,iffCE];
 
 (*Quantifier rules*)
-val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality] 
+val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality] 
                      addSEs [exE] addEs [allE];
 
 val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/equalities.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -104,8 +104,9 @@
 by (Blast_tac 1);
 qed "mk_disjoint_insert";
 
-bind_thm ("insert_Collect", prove_goal (the_context ())
-	  "insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
+Goal "insert a (Collect P) = {u. u ~= a --> P u}";
+by Auto_tac;
+qed "insert_Collect";
 
 Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
 by (Blast_tac 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/ex/PiSets.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -48,7 +48,7 @@
  by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 2);
   by (force_tac (claset(), simpset() addsimps [Graph_def]) 2);
  by (full_simp_tac (simpset() addsimps [Graph_def]) 2);
-  by (stac select_equality 2);
+  by (stac some_equality 2);
    by (assume_tac 2);
   by (Blast_tac 2);
  by (Blast_tac 2);
@@ -56,7 +56,7 @@
 by (full_simp_tac (simpset() addsimps [PiBij_def,Graph_def]) 1);
 by (stac restrict_apply1 1);
  by (rtac restrictI 1);
- by (blast_tac (claset() addSDs [[select_eq_Ex, ex1_implies_ex] MRS iffD2]) 1);
+ by (blast_tac (claset() addSDs [[some_eq_ex, ex1_implies_ex] MRS iffD2]) 1);
 (** LEVEL 17 **)
 by (rtac equalityI 1);
 by (rtac subsetI 1);
@@ -65,11 +65,11 @@
 by (Blast_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
 (*Blast_tac: PROOF FAILED for depth 5*)
-by (fast_tac (claset() addSIs [select1_equality RS sym]) 1);
+by (fast_tac (claset() addSIs [some1_equality RS sym]) 1);
 (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
-by (fast_tac (claset() addIs [selectI2]) 1);
+by (fast_tac (claset() addIs [someI2]) 1);
 qed "surj_PiBij";
 
 Goal "f: Pi A B ==> \
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/ex/Tarski.ML
--- a/src/HOL/ex/Tarski.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/ex/Tarski.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -273,7 +273,7 @@
 by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
 by (assume_tac 1);
 by (rewrite_goals_tac [lub_def,least_def]);
-by (stac select_equality 1);
+by (stac some_equality 1);
 by (rtac conjI 1);
 by (afs [islub_def] 2);
 by (etac conjunct2 2);
@@ -290,7 +290,7 @@
 by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
 by (assume_tac 1);
 by (rewrite_goals_tac [lub_def,least_def]);
-by (stac select_equality 1);
+by (stac some_equality 1);
 by (rtac conjI 1);
 by (afs [islub_def] 2);
 by (etac conjunct2 2);
@@ -315,7 +315,7 @@
 by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
 by (assume_tac 1);
 by (rewrite_goals_tac [lub_def,least_def]);
-by (stac select_equality 1);
+by (stac some_equality 1);
 by (afs [islub_def] 1);
 by (afs [islub_def, thm "A_def"] 2);
 by (rtac lub_unique 1);
@@ -701,7 +701,7 @@
 
 Goal "Bot cl: A";
 by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (fold_goals_tac [thm "A_def"]);
 by (etac conjunct1 2);
 by (rtac conjI 1);
@@ -719,7 +719,7 @@
 
 Goal "x: A ==> (x, Top cl): r";
 by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (fold_goals_tac [thm "r_def", thm "A_def"]);
 by (Fast_tac 2);
 by (rtac conjI 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/mono.ML
--- a/src/HOL/mono.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/mono.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -109,9 +109,9 @@
   "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
 \  ==> (LEAST y. y : f``S) = f(LEAST x. x : S)";
 by (etac bexE 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (Force_tac 1);
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (Force_tac 1);
 by (force_tac (claset() addSIs [order_antisym], simpset()) 1);
 qed "Least_mono";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/simpdata.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -380,7 +380,7 @@
        if_True, if_False, if_cancel, if_eq_cancel,
        imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
-       disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq,
+       disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial,
        thm"plus_ac0.zero", thm"plus_ac0_zero_right"]
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -249,7 +249,7 @@
   by (etac ballE 1);
   by (Blast_tac 2);
   by (etac exE 1);
-  by (rtac selectI2 1);
+  by (rtac someI2 1);
   by (assume_tac 1);
   by (Blast_tac 1);
 qed"simulation_starts";
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOLCF/Pcpo.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -12,7 +12,7 @@
 (* ------------------------------------------------------------------------ *)
  
 Goalw [UU_def] "ALL z. UU << z";
-by (rtac (select_eq_Ex RS iffD2) 1);
+by (rtac (some_eq_ex RS iffD2) 1);
 by (rtac least 1);
 qed "UU_least";
 
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOLCF/Porder0.ML
--- a/src/HOLCF/Porder0.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOLCF/Porder0.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -12,7 +12,7 @@
 (* minimal fixes least element                                              *)
 (* ------------------------------------------------------------------------ *)
 Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)";
-by (blast_tac (claset() addIs [selectI2,antisym_less]) 1);
+by (blast_tac (claset() addIs [someI2,antisym_less]) 1);
 bind_thm ("minimal2UU", allI RS result());
 
 (* ------------------------------------------------------------------------ *)
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOLCF/Sprod0.ML
--- a/src/HOLCF/Sprod0.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOLCF/Sprod0.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -158,7 +158,7 @@
 (* ------------------------------------------------------------------------ *)
 
 Goalw [Isfst_def] "p=Ispair UU UU ==> Isfst p = UU";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (rtac conjI 1);
 by (fast_tac HOL_cs  1);
 by (strip_tac 1);
@@ -187,7 +187,7 @@
 
 
 Goalw [Issnd_def] "p=Ispair UU UU ==>Issnd p=UU";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (rtac conjI 1);
 by (fast_tac HOL_cs  1);
 by (strip_tac 1);
@@ -214,7 +214,7 @@
 Addsimps [strict_Issnd2];
 
 Goalw [Isfst_def] "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (rtac conjI 1);
 by (strip_tac 1);
 by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
@@ -230,7 +230,7 @@
 qed "Isfst";
 
 Goalw [Issnd_def] "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (rtac conjI 1);
 by (strip_tac 1);
 by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOLCF/Ssum0.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -223,7 +223,7 @@
 
 Goalw [Iwhen_def]
         "Iwhen f g (Isinl UU) = UU";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (rtac conjI 1);
 by (fast_tac HOL_cs  1);
 by (rtac conjI 1);
@@ -246,7 +246,7 @@
 
 Goalw [Iwhen_def]
         "x~=UU ==> Iwhen f g (Isinl x) = f`x";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (fast_tac HOL_cs  2);
 by (rtac conjI 1);
 by (strip_tac 1);
@@ -269,7 +269,7 @@
 
 Goalw [Iwhen_def]
         "y~=UU ==> Iwhen f g (Isinr y) = g`y";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (fast_tac HOL_cs  2);
 by (rtac conjI 1);
 by (strip_tac 1);
diff -r 264b16d934f9 -r 4753185f1dd2 src/HOLCF/Ssum1.ML
--- a/src/HOLCF/Ssum1.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOLCF/Ssum1.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -36,7 +36,7 @@
 
 Goalw [less_ssum_def]
 "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (dtac conjunct1 2);
 by (dtac spec 2);
 by (dtac spec 2);
@@ -74,7 +74,7 @@
 
 Goalw [less_ssum_def]
 "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (dtac conjunct2 2);
 by (dtac conjunct1 2);
 by (dtac spec 2);
@@ -113,7 +113,7 @@
 
 Goalw [less_ssum_def]
 "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (rtac conjI 1);
 by (strip_tac 1);
 by (etac conjE 1);
@@ -152,7 +152,7 @@
 
 Goalw [less_ssum_def]
 "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)";
-by (rtac select_equality 1);
+by (rtac some_equality 1);
 by (dtac conjunct2 2);
 by (dtac conjunct2 2);
 by (dtac conjunct2 2);