renamed (most of...) the select rules
authorpaulson
Fri Sep 15 12:39:57 2000 +0200 (2000-09-15)
changeset 99694753185f1dd2
parent 9968 264b16d934f9
child 9970 dfe4747c8318
renamed (most of...) the select rules
doc-src/HOL/HOL.tex
src/HOL/AxClasses/Lattice/CLattice.ML
src/HOL/BCV/Semilat.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/HOL_lemmas.ML
src/HOL/Hoare/Arith2.ML
src/HOL/Integ/Bin.ML
src/HOL/MicroJava/J/JBasis.ML
src/HOL/MicroJava/JVM/Store.ML
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/NumberTheory/IntPrimes.ML
src/HOL/Ord.ML
src/HOL/Prod.ML
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/FunctionOrder.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/Hyperreal/Zorn.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RealDef.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/typedef_package.ML
src/HOL/Trancl.ML
src/HOL/UNITY/Extend.ML
src/HOL/Univ.ML
src/HOL/Vimage.ML
src/HOL/WF_Rel.ML
src/HOL/cladata.ML
src/HOL/equalities.ML
src/HOL/ex/PiSets.ML
src/HOL/ex/Tarski.ML
src/HOL/mono.ML
src/HOL/simpdata.ML
src/HOLCF/IOA/meta_theory/SimCorrectness.ML
src/HOLCF/Pcpo.ML
src/HOLCF/Porder0.ML
src/HOLCF/Sprod0.ML
src/HOLCF/Ssum0.ML
src/HOLCF/Ssum1.ML
     1.1 --- a/doc-src/HOL/HOL.tex	Fri Sep 15 11:34:46 2000 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Fri Sep 15 12:39:57 2000 +0200
     1.3 @@ -290,7 +290,7 @@
     1.4  \tdx{impI}          (P ==> Q) ==> P-->Q
     1.5  \tdx{mp}            [| P-->Q;  P |] ==> Q
     1.6  \tdx{iff}           (P-->Q) --> (Q-->P) --> (P=Q)
     1.7 -\tdx{selectI}       P(x::'a) ==> P(@x. P x)
     1.8 +\tdx{someI}         P(x::'a) ==> P(@x. P x)
     1.9  \tdx{True_or_False} (P=True) | (P=False)
    1.10  \end{ttbox}
    1.11  \caption{The \texttt{HOL} rules} \label{hol-rules}
    1.12 @@ -302,9 +302,9 @@
    1.13  \item[\tdx{ext}] expresses extensionality of functions.
    1.14  \item[\tdx{iff}] asserts that logically equivalent formulae are
    1.15    equal.
    1.16 -\item[\tdx{selectI}] gives the defining property of the Hilbert
    1.17 +\item[\tdx{someI}] gives the defining property of the Hilbert
    1.18    $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule
    1.19 -  \tdx{select_equality} (see below) is often easier to use.
    1.20 +  \tdx{some_equality} (see below) is often easier to use.
    1.21  \item[\tdx{True_or_False}] makes the logic classical.\footnote{In
    1.22      fact, the $\varepsilon$-operator already makes the logic classical, as
    1.23      shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
    1.24 @@ -409,7 +409,7 @@
    1.25  \tdx{ex1E}      [| ?! x. P x;  !!x. [| P x;  ! y. P y --> y=x |] ==> R 
    1.26            |] ==> R
    1.27  
    1.28 -\tdx{select_equality} [| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a
    1.29 +\tdx{some_equality}   [| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a
    1.30  \subcaption{Quantifiers and descriptions}
    1.31  
    1.32  \tdx{ccontr}          (~P ==> False) ==> P
     2.1 --- a/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Sep 15 11:34:46 2000 +0200
     2.2 +++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Sep 15 12:39:57 2000 +0200
     2.3 @@ -51,14 +51,14 @@
     2.4  
     2.5  val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
     2.6    by (cut_facts_tac prems 1);
     2.7 -  by (rtac selectI2 1);
     2.8 +  by (rtac someI2 1);
     2.9    by (rtac Inf_is_Inf 1);
    2.10    by (rewtac is_Inf_def);
    2.11    by (Fast_tac 1);
    2.12  qed "Inf_lb";
    2.13  
    2.14  val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
    2.15 -  by (rtac selectI2 1);
    2.16 +  by (rtac someI2 1);
    2.17    by (rtac Inf_is_Inf 1);
    2.18    by (rewtac is_Inf_def);
    2.19    by (Step_tac 1);
    2.20 @@ -71,14 +71,14 @@
    2.21  
    2.22  val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
    2.23    by (cut_facts_tac prems 1);
    2.24 -  by (rtac selectI2 1);
    2.25 +  by (rtac someI2 1);
    2.26    by (rtac Sup_is_Sup 1);
    2.27    by (rewtac is_Sup_def);
    2.28    by (Fast_tac 1);
    2.29  qed "Sup_ub";
    2.30  
    2.31  val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
    2.32 -  by (rtac selectI2 1);
    2.33 +  by (rtac someI2 1);
    2.34    by (rtac Sup_is_Sup 1);
    2.35    by (rewtac is_Sup_def);
    2.36    by (Step_tac 1);
     3.1 --- a/src/HOL/BCV/Semilat.ML	Fri Sep 15 11:34:46 2000 +0200
     3.2 +++ b/src/HOL/BCV/Semilat.ML	Fri Sep 15 12:39:57 2000 +0200
     3.3 @@ -162,7 +162,7 @@
     3.4  
     3.5  Goalw [some_lub_def,is_lub_def]
     3.6   "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u";
     3.7 -br selectI2 1;
     3.8 +br someI2 1;
     3.9   ba 1;
    3.10  by(blast_tac (claset() addIs [antisymD]
    3.11                         addSDs [acyclic_impl_antisym_rtrancl]) 1);
     4.1 --- a/src/HOL/Finite.ML	Fri Sep 15 11:34:46 2000 +0200
     4.2 +++ b/src/HOL/Finite.ML	Fri Sep 15 12:39:57 2000 +0200
     4.3 @@ -323,7 +323,7 @@
     4.4  Goalw [card_def]
     4.5       "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)";
     4.6  by (asm_simp_tac (simpset() addsimps [lemma]) 1);
     4.7 -by (rtac select_equality 1);
     4.8 +by (rtac some_equality 1);
     4.9  by (auto_tac (claset() addIs [finite_imp_cardR],
    4.10  	      simpset() addcongs [conj_cong]
    4.11  		        addsimps [symmetric card_def,
    4.12 @@ -596,7 +596,7 @@
    4.13  Goalw [fold_def]
    4.14       "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)";
    4.15  by (asm_simp_tac (simpset() addsimps [lemma]) 1);
    4.16 -by (rtac select_equality 1);
    4.17 +by (rtac some_equality 1);
    4.18  by (auto_tac (claset() addIs [finite_imp_foldSet],
    4.19  	      simpset() addcongs [conj_cong]
    4.20  		        addsimps [symmetric fold_def,
     5.1 --- a/src/HOL/Fun.ML	Fri Sep 15 11:34:46 2000 +0200
     5.2 +++ b/src/HOL/Fun.ML	Fri Sep 15 12:39:57 2000 +0200
     5.3 @@ -584,7 +584,7 @@
     5.4  
     5.5  Goalw [Inv_def] "[| f `` A = B; f : A funcset B |] \
     5.6  \                ==> (lam x: B. (Inv A f) x) : B funcset A";
     5.7 -by (fast_tac (claset() addIs [restrict_in_funcset, selectI2]) 1);
     5.8 +by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
     5.9  qed "Inv_funcset";
    5.10  
    5.11  
    5.12 @@ -592,14 +592,14 @@
    5.13  \     ==> (lam y: B. (Inv A f) y) (f x) = x";
    5.14  by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
    5.15  by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
    5.16 -by (rtac selectI2 1);
    5.17 +by (rtac someI2 1);
    5.18  by Auto_tac;
    5.19  qed "Inv_f_f";
    5.20  
    5.21  Goal "[| f: A funcset B;  f `` A = B;  x: B |] \
    5.22  \     ==> f ((lam y: B. (Inv A f y)) x) = x";
    5.23  by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
    5.24 -by (fast_tac (claset() addIs [selectI2]) 1);
    5.25 +by (fast_tac (claset() addIs [someI2]) 1);
    5.26  qed "f_Inv_f";
    5.27  
    5.28  Goal "[| f: A funcset B;  inj_on f A;  f `` A = B |]\
     6.1 --- a/src/HOL/HOL_lemmas.ML	Fri Sep 15 11:34:46 2000 +0200
     6.2 +++ b/src/HOL/HOL_lemmas.ML	Fri Sep 15 12:39:57 2000 +0200
     6.3 @@ -49,7 +49,7 @@
     6.4  by (etac subst 1 THEN assume_tac 1);
     6.5  qed "trans";
     6.6  
     6.7 -val prems = goal (the_context ()) "(A == B) ==> A = B";
     6.8 +val prems = goal (the_context()) "(A == B) ==> A = B";
     6.9  by (rewrite_goals_tac prems);
    6.10  by (rtac refl 1);
    6.11  qed "def_imp_eq";
    6.12 @@ -140,11 +140,11 @@
    6.13  by (etac fun_cong 1);
    6.14  qed "spec";
    6.15  
    6.16 -val major::prems= goal (the_context ()) "[| ALL x. P(x);  P(x) ==> R |] ==> R";
    6.17 +val major::prems = Goal "[| ALL x. P(x);  P(x) ==> R |] ==> R";
    6.18  by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
    6.19  qed "allE";
    6.20  
    6.21 -val prems = goal (the_context ())
    6.22 +val prems = Goal
    6.23      "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
    6.24  by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
    6.25  qed "all_dupE";
    6.26 @@ -356,7 +356,7 @@
    6.27  section "@";
    6.28  
    6.29  (*Easier to apply than selectI if witness ?a comes from an EX-formula*)
    6.30 -Goal "EX a. P a ==> P (SOME x. P x)";
    6.31 +Goal "EX x. P x ==> P (SOME x. P x)";
    6.32  by (etac exE 1);
    6.33  by (etac selectI 1);
    6.34  qed "ex_someI";
    6.35 @@ -367,22 +367,22 @@
    6.36  by (resolve_tac prems 1);
    6.37  by (rtac selectI 1);
    6.38  by (resolve_tac prems 1) ;
    6.39 -qed "selectI2";
    6.40 +qed "someI2";
    6.41  
    6.42 -(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
    6.43 +(*Easier to apply than someI2 if witness ?a comes from an EX-formula*)
    6.44  val [major,minor] = Goal "[| EX a. P a;  !!x. P x ==> Q x |] ==> Q (Eps P)";
    6.45  by (rtac (major RS exE) 1);
    6.46 -by (etac selectI2 1 THEN etac minor 1);
    6.47 -qed "selectI2EX";
    6.48 +by (etac someI2 1 THEN etac minor 1);
    6.49 +qed "someI2EX";
    6.50  
    6.51  val prems = Goal
    6.52      "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a";
    6.53 -by (rtac selectI2 1);
    6.54 +by (rtac someI2 1);
    6.55  by (REPEAT (ares_tac prems 1)) ;
    6.56 -qed "select_equality";
    6.57 +qed "some_equality";
    6.58  
    6.59  Goalw [Ex1_def] "[| EX!x. P x; P a |] ==> (@x. P x) = a";
    6.60 -by (rtac select_equality 1);
    6.61 +by (rtac some_equality 1);
    6.62  by (atac 1);
    6.63  by (etac exE 1);
    6.64  by (etac conjE 1);
    6.65 @@ -394,31 +394,31 @@
    6.66  by (etac allE 1);
    6.67  by (etac mp 1);
    6.68  by (atac 1);
    6.69 -qed "select1_equality";
    6.70 +qed "some1_equality";
    6.71  
    6.72  Goal "P (@ x. P x) =  (EX x. P x)";
    6.73  by (rtac iffI 1);
    6.74  by (etac exI 1);
    6.75  by (etac exE 1);
    6.76  by (etac selectI 1);
    6.77 -qed "select_eq_Ex";
    6.78 +qed "some_eq_ex";
    6.79  
    6.80  Goal "(@y. y=x) = x";
    6.81 -by (rtac select_equality 1);
    6.82 +by (rtac some_equality 1);
    6.83  by (rtac refl 1);
    6.84  by (atac 1);
    6.85 -qed "Eps_eq";
    6.86 +qed "some_eq_trivial";
    6.87  
    6.88 -Goal "(Eps (op = x)) = x";
    6.89 -by (rtac select_equality 1);
    6.90 +Goal "(@y. x=y) = x";
    6.91 +by (rtac some_equality 1);
    6.92  by (rtac refl 1);
    6.93  by (etac sym 1);
    6.94 -qed "Eps_sym_eq";
    6.95 +qed "some_sym_eq_trivial";
    6.96  
    6.97  (** Classical intro rules for disjunction and existential quantifiers *)
    6.98  section "classical intro rules";
    6.99  
   6.100 -val prems= Goal "(~Q ==> P) ==> P|Q";
   6.101 +val prems = Goal "(~Q ==> P) ==> P|Q";
   6.102  by (rtac classical 1);
   6.103  by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
   6.104  by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
     7.1 --- a/src/HOL/Hoare/Arith2.ML	Fri Sep 15 11:34:46 2000 +0200
     7.2 +++ b/src/HOL/Hoare/Arith2.ML	Fri Sep 15 12:39:57 2000 +0200
     7.3 @@ -37,7 +37,7 @@
     7.4  
     7.5  Goalw [gcd_def] "0<n ==> n = gcd n n";
     7.6  by (ftac cd_nnn 1);
     7.7 -by (rtac (select_equality RS sym) 1);
     7.8 +by (rtac (some_equality RS sym) 1);
     7.9  by (blast_tac (claset() addDs [cd_le]) 1);
    7.10  by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1);
    7.11  qed "gcd_nnn";
     8.1 --- a/src/HOL/Integ/Bin.ML	Fri Sep 15 11:34:46 2000 +0200
     8.2 +++ b/src/HOL/Integ/Bin.ML	Fri Sep 15 12:39:57 2000 +0200
     8.3 @@ -281,7 +281,7 @@
     8.4  by Auto_tac;
     8.5  qed "zmult_0_eq_iff";
     8.6  
     8.7 -Addsimps [zmult_eq_0_iff, zmult_0_eq_iff];
     8.8 +AddIffs [zmult_eq_0_iff, zmult_0_eq_iff];
     8.9  
    8.10  Goal "(w < z + (#1::int)) = (w<z | w=z)";
    8.11  by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
     9.1 --- a/src/HOL/MicroJava/J/JBasis.ML	Fri Sep 15 11:34:46 2000 +0200
     9.2 +++ b/src/HOL/MicroJava/J/JBasis.ML	Fri Sep 15 12:39:57 2000 +0200
     9.3 @@ -43,10 +43,10 @@
     9.4  
     9.5  (* To HOL.ML *)
     9.6  
     9.7 -val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" 
     9.8 +val ex1_some_eq_trivial = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" 
     9.9  	(fn prems => [
    9.10  	cut_facts_tac prems 1,
    9.11 -	rtac select_equality 1,
    9.12 +	rtac some_equality 1,
    9.13  	 atac 1,
    9.14  	etac ex1E 1,
    9.15  	etac all_dupE 1,
    10.1 --- a/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 11:34:46 2000 +0200
    10.2 +++ b/src/HOL/MicroJava/JVM/Store.ML	Fri Sep 15 12:39:57 2000 +0200
    10.3 @@ -6,5 +6,5 @@
    10.4  
    10.5  Goalw [newref_def]
    10.6   "hp x = None \\<longrightarrow> hp (newref hp) = None";
    10.7 -by (fast_tac (claset() addIs [selectI2EX] addss (simpset())) 1);
    10.8 +by (fast_tac (claset() addIs [someI2EX] addss (simpset())) 1);
    10.9  qed_spec_mp "newref_None";
    11.1 --- a/src/HOL/Nat.ML	Fri Sep 15 11:34:46 2000 +0200
    11.2 +++ b/src/HOL/Nat.ML	Fri Sep 15 12:39:57 2000 +0200
    11.3 @@ -76,7 +76,7 @@
    11.4  
    11.5  Goalw [Least_nat_def]
    11.6   "[| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
    11.7 -by (rtac select_equality 1);
    11.8 +by (rtac some_equality 1);
    11.9  by (fold_goals_tac [Least_nat_def]);
   11.10  by (safe_tac (claset() addSEs [LeastI]));
   11.11  by (rename_tac "j" 1);
   11.12 @@ -88,7 +88,7 @@
   11.13  by (Blast_tac 1);
   11.14  by (hyp_subst_tac 1);
   11.15  by (rewtac Least_nat_def);
   11.16 -by (rtac (select_equality RS arg_cong RS sym) 1);
   11.17 +by (rtac (some_equality RS arg_cong RS sym) 1);
   11.18  by (blast_tac (claset() addDs [Suc_mono]) 1);
   11.19  by (cut_inst_tac [("m","m")] less_linear 1);
   11.20  by (blast_tac (claset() addIs [Suc_mono]) 1);
    12.1 --- a/src/HOL/NatDef.ML	Fri Sep 15 11:34:46 2000 +0200
    12.2 +++ b/src/HOL/NatDef.ML	Fri Sep 15 12:39:57 2000 +0200
    12.3 @@ -476,7 +476,7 @@
    12.4  
    12.5  val [prem1,prem2] = Goalw [Least_nat_def]
    12.6      "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
    12.7 -by (rtac select_equality 1);
    12.8 +by (rtac some_equality 1);
    12.9  by (blast_tac (claset() addSIs [prem1,prem2]) 1);
   12.10  by (cut_facts_tac [less_linear] 1);
   12.11  by (blast_tac (claset() addSIs [prem1] addSDs [prem2]) 1);
    13.1 --- a/src/HOL/NumberTheory/IntPrimes.ML	Fri Sep 15 11:34:46 2000 +0200
    13.2 +++ b/src/HOL/NumberTheory/IntPrimes.ML	Fri Sep 15 12:39:57 2000 +0200
    13.3 @@ -569,7 +569,7 @@
    13.4  by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
    13.5  by (subgoal_tac "m*k<m*#1" 1);
    13.6  by (dtac (zmult_zless_cancel1 RS iffD1) 1);
    13.7 -by Auto_tac;  
    13.8 +by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
    13.9  qed "zcong_zless_0";
   13.10  
   13.11  Goal "#0<m ==> (EX! b. #0<=b & b<m & [a = b] (mod m))";
    14.1 --- a/src/HOL/Ord.ML	Fri Sep 15 11:34:46 2000 +0200
    14.2 +++ b/src/HOL/Ord.ML	Fri Sep 15 12:39:57 2000 +0200
    14.3 @@ -120,10 +120,9 @@
    14.4  by (Blast_tac 1);
    14.5  qed "linorder_less_linear";
    14.6  
    14.7 -val prems = goal (the_context ())
    14.8 - "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
    14.9 -by(cut_facts_tac [linorder_less_linear] 1);
   14.10 -by(REPEAT(eresolve_tac (prems@[disjE]) 1));
   14.11 +val prems = Goal "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
   14.12 +by (cut_facts_tac [linorder_less_linear] 1);
   14.13 +by (REPEAT(eresolve_tac (prems@[disjE]) 1));
   14.14  qed "linorder_less_split";
   14.15  
   14.16  Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
    15.1 --- a/src/HOL/Prod.ML	Fri Sep 15 11:34:46 2000 +0200
    15.2 +++ b/src/HOL/Prod.ML	Fri Sep 15 12:39:57 2000 +0200
    15.3 @@ -55,10 +55,9 @@
    15.4  by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
    15.5  qed "ProdI";
    15.6  
    15.7 -val [major] = goalw (the_context ()) [Pair_Rep_def]
    15.8 -    "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
    15.9 -by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst),
   15.10 -            rtac conjI, rtac refl, rtac refl]);
   15.11 +Goalw [Pair_Rep_def] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
   15.12 +by (dtac (fun_cong RS fun_cong) 1);
   15.13 +by (Blast_tac 1);
   15.14  qed "Pair_Rep_inject";
   15.15  
   15.16  Goal "inj_on Abs_Prod Prod";
   15.17 @@ -185,9 +184,8 @@
   15.18  qed "Pair_fst_snd_eq";
   15.19  
   15.20  (*Prevents simplification of c: much faster*)
   15.21 -val [prem] = goal (the_context ())
   15.22 -  "p=q ==> split c p = split c q";
   15.23 -by (rtac (prem RS arg_cong) 1);
   15.24 +Goal "p=q ==> split c p = split c q";
   15.25 +by (etac arg_cong 1);
   15.26  qed "split_weak_cong";
   15.27  
   15.28  Goal "(%(x,y). f(x,y)) = f";
   15.29 @@ -303,7 +301,7 @@
   15.30  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   15.31  qed "splitE'";
   15.32  
   15.33 -val major::prems = goal (the_context ())
   15.34 +val major::prems = Goal
   15.35      "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R  \
   15.36  \    |] ==> R";
   15.37  by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
   15.38 @@ -360,7 +358,7 @@
   15.39  ### Cannot add premise as rewrite rule because it contains (type) unknowns:
   15.40  ### ?y = .x
   15.41  Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
   15.42 -by (rtac select_equality 1);
   15.43 +by (rtac some_equality 1);
   15.44  by ( Simp_tac 1);
   15.45  by (split_all_tac 1);
   15.46  by (Asm_full_simp_tac 1);
   15.47 @@ -436,7 +434,7 @@
   15.48  by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
   15.49  qed "SigmaD2";
   15.50  
   15.51 -val [major,minor]= goal (the_context ())
   15.52 +val [major,minor]= Goal
   15.53      "[| (a,b) : Sigma A B;    \
   15.54  \       [| a:A;  b:B(a) |] ==> P   \
   15.55  \    |] ==> P";
    16.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 11:34:46 2000 +0200
    16.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 12:39:57 2000 +0200
    16.3 @@ -97,7 +97,7 @@
    16.4    "[| is_normed_vectorspace V norm; is_continuous V norm f|]
    16.5       ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
    16.6  proof (unfold function_norm_def is_function_norm_def 
    16.7 -  is_continuous_def Sup_def, elim conjE, rule selectI2EX)
    16.8 +  is_continuous_def Sup_def, elim conjE, rule someI2EX)
    16.9    assume "is_normed_vectorspace V norm"
   16.10    assume "is_linearform V f" 
   16.11    and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
    17.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Sep 15 11:34:46 2000 +0200
    17.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Sep 15 12:39:57 2000 +0200
    17.3 @@ -75,11 +75,11 @@
    17.4    ==> graph (domain g) (funct g) = g"
    17.5  proof (unfold domain_def funct_def graph_def, auto)
    17.6    fix a b assume "(a, b) \<in> g"
    17.7 -  show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule selectI2)
    17.8 +  show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
    17.9    show "\<exists>y. (a, y) \<in> g" ..
   17.10    assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
   17.11    show "b = (SOME y. (a, y) \<in> g)"
   17.12 -  proof (rule select_equality [symmetric])
   17.13 +  proof (rule some_equality [symmetric])
   17.14      fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
   17.15    qed
   17.16  qed
    18.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Sep 15 11:34:46 2000 +0200
    18.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Sep 15 12:39:57 2000 +0200
    18.3 @@ -469,7 +469,7 @@
    18.4      qed
    18.5    qed
    18.6    hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
    18.7 -    by (rule select1_equality) (force!)
    18.8 +    by (rule some1_equality) (force!)
    18.9    thus "h' x = h y + a * xi" by (simp! add: Let_def)
   18.10  qed
   18.11  
    19.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Fri Sep 15 11:34:46 2000 +0200
    19.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Fri Sep 15 12:39:57 2000 +0200
    19.3 @@ -43,13 +43,13 @@
    19.4  Goalw [FreeUltrafilterNat_def] 
    19.5       "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)";
    19.6  by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    19.7 -by (rtac selectI2 1 THEN ALLGOALS(assume_tac));
    19.8 +by (rtac someI2 1 THEN ALLGOALS(assume_tac));
    19.9  qed "FreeUltrafilterNat_mem";
   19.10  Addsimps [FreeUltrafilterNat_mem];
   19.11  
   19.12  Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat";
   19.13  by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
   19.14 -by (rtac selectI2 1 THEN assume_tac 1);
   19.15 +by (rtac someI2 1 THEN assume_tac 1);
   19.16  by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1);
   19.17  qed "FreeUltrafilterNat_finite";
   19.18  
   19.19 @@ -59,7 +59,7 @@
   19.20  
   19.21  Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat";
   19.22  by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
   19.23 -by (rtac selectI2 1 THEN assume_tac 1);
   19.24 +by (rtac someI2 1 THEN assume_tac 1);
   19.25  by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
   19.26  			       Ultrafilter_Filter,Filter_empty_not_mem]) 1);
   19.27  qed "FreeUltrafilterNat_empty";
    20.1 --- a/src/HOL/Real/Hyperreal/Zorn.ML	Fri Sep 15 11:34:46 2000 +0200
    20.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Fri Sep 15 12:39:57 2000 +0200
    20.3 @@ -32,7 +32,7 @@
    20.4  by (auto_tac (claset(),simpset() addsimps [super_def,
    20.5                 maxchain_def,psubset_def]));
    20.6  by (rtac swap 1 THEN assume_tac 1);
    20.7 -by (rtac selectI2 1);
    20.8 +by (rtac someI2 1);
    20.9  by (ALLGOALS(Blast_tac));
   20.10  qed "Abrial_axiom1";
   20.11  
   20.12 @@ -167,7 +167,7 @@
   20.13  Goal "c: chain S - maxchain S ==> \
   20.14  \                         (@c'. c': super S c): super S c";
   20.15  by (etac (mem_super_Ex RS exE) 1);
   20.16 -by (rtac selectI2 1);
   20.17 +by (rtac someI2 1);
   20.18  by (Auto_tac);
   20.19  qed "select_super";
   20.20  
    21.1 --- a/src/HOL/Real/PRat.ML	Fri Sep 15 11:34:46 2000 +0200
    21.2 +++ b/src/HOL/Real/PRat.ML	Fri Sep 15 12:39:57 2000 +0200
    21.3 @@ -38,7 +38,7 @@
    21.4  by (Fast_tac 1);
    21.5  qed "ratrelE_lemma";
    21.6  
    21.7 -val [major,minor] = goal (the_context ())
    21.8 +val [major,minor] = Goal
    21.9    "[| p: ratrel;  \
   21.10  \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1*y2 = x2*y1 \
   21.11  \                    |] ==> Q |] ==> Q";
   21.12 @@ -96,7 +96,7 @@
   21.13  by (Asm_full_simp_tac 1);
   21.14  qed "inj_prat_of_pnat";
   21.15  
   21.16 -val [prem] = goal (the_context ())
   21.17 +val [prem] = Goal
   21.18      "(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P";
   21.19  by (res_inst_tac [("x1","z")] 
   21.20      (rewrite_rule [prat_def] Rep_prat RS quotientE) 1);
   21.21 @@ -611,7 +611,7 @@
   21.22  by (simp_tac (simpset() addsimps [prat_le_eq_less_or_eq]) 1);
   21.23  qed "prat_le_refl";
   21.24  
   21.25 -val prems = goal (the_context ()) "!!i. [| i <= j; j < k |] ==> i < (k::prat)";
   21.26 +Goal "[| i <= j; j < k |] ==> i < (k::prat)";
   21.27  by (dtac prat_le_imp_less_or_eq 1);
   21.28  by (fast_tac (claset() addIs [prat_less_trans]) 1);
   21.29  qed "prat_le_less_trans";
    22.1 --- a/src/HOL/Real/PReal.ML	Fri Sep 15 11:34:46 2000 +0200
    22.2 +++ b/src/HOL/Real/PReal.ML	Fri Sep 15 12:39:57 2000 +0200
    22.3 @@ -698,7 +698,7 @@
    22.4  by (rtac preal_mult_inv 1);
    22.5  qed "preal_mult_inv_right";
    22.6  
    22.7 -val [prem] = goal (the_context ())
    22.8 +val [prem] = Goal
    22.9      "(!!u. z = Abs_preal(u) ==> P) ==> P";
   22.10  by (cut_inst_tac [("x1","z")] 
   22.11      (rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1);
   22.12 @@ -779,12 +779,12 @@
   22.13  by (Simp_tac 1);
   22.14  qed "preal_le_refl";
   22.15  
   22.16 -val prems = goal (the_context ()) "!!i. [| i <= j; j < k |] ==> i < (k::preal)";
   22.17 +Goal "[| i <= j; j < k |] ==> i < (k::preal)";
   22.18  by (dtac preal_le_imp_less_or_eq 1);
   22.19  by (fast_tac (claset() addIs [preal_less_trans]) 1);
   22.20  qed "preal_le_less_trans";
   22.21  
   22.22 -val prems = goal (the_context ()) "!!i. [| i < j; j <= k |] ==> i < (k::preal)";
   22.23 +Goal "[| i < j; j <= k |] ==> i < (k::preal)";
   22.24  by (dtac preal_le_imp_less_or_eq 1);
   22.25  by (fast_tac (claset() addIs [preal_less_trans]) 1);
   22.26  qed "preal_less_le_trans";
   22.27 @@ -804,7 +804,7 @@
   22.28  by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
   22.29  qed "not_less_not_eq_preal_less";
   22.30  
   22.31 -(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
   22.32 +(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
   22.33  
   22.34  (**** Set up all lemmas for proving A < B ==> ?D. A + D = B ****)
   22.35  (**** Gleason prop. 9-3.5(iv) p. 123 ****)
    23.1 --- a/src/HOL/Real/RealDef.ML	Fri Sep 15 11:34:46 2000 +0200
    23.2 +++ b/src/HOL/Real/RealDef.ML	Fri Sep 15 12:39:57 2000 +0200
    23.3 @@ -35,7 +35,7 @@
    23.4  by (Blast_tac 1);
    23.5  qed "realrelE_lemma";
    23.6  
    23.7 -val [major,minor] = goal (the_context ())
    23.8 +val [major,minor] = Goal
    23.9    "[| p: realrel;  \
   23.10  \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1 \
   23.11  \                    |] ==> Q |] ==> Q";
   23.12 @@ -94,7 +94,7 @@
   23.13  by (Asm_full_simp_tac 1);
   23.14  qed "inj_real_of_preal";
   23.15  
   23.16 -val [prem] = goal (the_context ())
   23.17 +val [prem] = Goal
   23.18      "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
   23.19  by (res_inst_tac [("x1","z")] 
   23.20      (rewrite_rule [real_def] Rep_real RS quotientE) 1);
   23.21 @@ -500,7 +500,7 @@
   23.22  Goalw [rinv_def] "x ~= 0 ==> rinv(x)*x = 1r";
   23.23  by (ftac real_mult_inv_left_ex 1);
   23.24  by (Step_tac 1);
   23.25 -by (rtac selectI2 1);
   23.26 +by (rtac someI2 1);
   23.27  by Auto_tac;
   23.28  qed "real_mult_inv_left";
   23.29  
   23.30 @@ -533,7 +533,7 @@
   23.31  Goalw [rinv_def] "x ~= 0 ==> rinv(x) ~= 0";
   23.32  by (ftac real_mult_inv_left_ex 1);
   23.33  by (etac exE 1);
   23.34 -by (rtac selectI2 1);
   23.35 +by (rtac someI2 1);
   23.36  by (auto_tac (claset(),
   23.37  	      simpset() addsimps [real_mult_0,
   23.38      real_zero_not_eq_one]));
    24.1 --- a/src/HOL/Relation.ML	Fri Sep 15 11:34:46 2000 +0200
    24.2 +++ b/src/HOL/Relation.ML	Fri Sep 15 12:39:57 2000 +0200
    24.3 @@ -442,12 +442,12 @@
    24.4  by (rtac CollectI 1);
    24.5  by (rtac allI 1);
    24.6  by (etac allE 1);
    24.7 -by (rtac (select_eq_Ex RS iffD2) 1);
    24.8 +by (rtac (some_eq_ex RS iffD2) 1);
    24.9  by (etac ex1_implies_ex 1);
   24.10  by (rtac ext 1);
   24.11  by (etac CollectE 1);
   24.12  by (REPEAT (etac allE 1));
   24.13 -by (rtac (select1_equality RS sym) 1);
   24.14 +by (rtac (some1_equality RS sym) 1);
   24.15  by (atac 1);
   24.16  by (atac 1);
   24.17  qed "fun_rel_comp_unique";
    25.1 --- a/src/HOL/Set.ML	Fri Sep 15 11:34:46 2000 +0200
    25.2 +++ b/src/HOL/Set.ML	Fri Sep 15 12:39:57 2000 +0200
    25.3 @@ -720,13 +720,11 @@
    25.4  
    25.5  (*Split ifs on either side of the membership relation.
    25.6  	Not for Addsimps -- can cause goals to blow up!*)
    25.7 -bind_thm ("split_if_mem1", 
    25.8 -    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. x : ?b")] split_if);
    25.9 -bind_thm ("split_if_mem2", 
   25.10 -    read_instantiate_sg (Theory.sign_of (the_context ())) [("P", "%x. ?a : x")] split_if);
   25.11 +bind_thm ("split_if_mem1", inst "P" "%x. x : ?b" split_if);
   25.12 +bind_thm ("split_if_mem2", inst "P" "%x. ?a : x" split_if);
   25.13  
   25.14  bind_thms ("split_ifs", [if_bool_eq_conj, split_if_eq1, split_if_eq2,
   25.15 -		  split_if_mem1, split_if_mem2]);
   25.16 +			 split_if_mem1, split_if_mem2]);
   25.17  
   25.18  
   25.19  (*Each of these has ALREADY been added to simpset() above.*)
    26.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 15 11:34:46 2000 +0200
    26.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Sep 15 12:39:57 2000 +0200
    26.3 @@ -245,7 +245,7 @@
    26.4        end;
    26.5  
    26.6      val rec_total_thms = map (fn r =>
    26.7 -      r RS ex1_implies_ex RS (select_eq_Ex RS iffD2)) rec_unique_thms;
    26.8 +      r RS ex1_implies_ex RS (some_eq_ex RS iffD2)) rec_unique_thms;
    26.9  
   26.10      (* define primrec combinators *)
   26.11  
   26.12 @@ -276,7 +276,7 @@
   26.13  
   26.14      val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
   26.15        (cterm_of (Theory.sign_of thy2) t) (fn _ =>
   26.16 -        [rtac select1_equality 1,
   26.17 +        [rtac some1_equality 1,
   26.18           resolve_tac rec_unique_thms 1,
   26.19           resolve_tac rec_intrs 1,
   26.20           rewrite_goals_tac [o_def, fun_rel_comp_def],
    27.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Sep 15 11:34:46 2000 +0200
    27.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Sep 15 12:39:57 2000 +0200
    27.3 @@ -193,7 +193,7 @@
    27.4  (* typedef_proof interface *)
    27.5  
    27.6  fun typedef_attribute cset do_typedef (thy, thm) =
    27.7 -  (check_nonempty cset (thm RS (select_eq_Ex RS iffD2)); (thy |> do_typedef, thm));
    27.8 +  (check_nonempty cset (thm RS (some_eq_ex RS iffD2)); (thy |> do_typedef, thm));
    27.9  
   27.10  fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
   27.11    let
    28.1 --- a/src/HOL/Trancl.ML	Fri Sep 15 11:34:46 2000 +0200
    28.2 +++ b/src/HOL/Trancl.ML	Fri Sep 15 12:39:57 2000 +0200
    28.3 @@ -254,7 +254,7 @@
    28.4  qed "trancl_induct";
    28.5  
    28.6  (*Another induction rule for trancl, incorporating transitivity.*)
    28.7 -val major::prems = goal (the_context ())
    28.8 +val major::prems = Goal
    28.9   "[| (x,y) : r^+; \
   28.10  \    !!x y. (x,y) : r ==> P x y; \
   28.11  \    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
    29.1 --- a/src/HOL/UNITY/Extend.ML	Fri Sep 15 11:34:46 2000 +0200
    29.2 +++ b/src/HOL/UNITY/Extend.ML	Fri Sep 15 12:39:57 2000 +0200
    29.3 @@ -88,7 +88,7 @@
    29.4  val [surj,prem] = Goalw [inv_def]
    29.5       "[| surj h;  !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z";
    29.6  by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1);
    29.7 -by (rtac selectI2 1);
    29.8 +by (rtac someI2 1);
    29.9  by (dres_inst_tac [("f", "g")] arg_cong 2);
   29.10  by (auto_tac (claset(), simpset() addsimps [prem]));
   29.11  qed "fst_inv_equalityI";
    30.1 --- a/src/HOL/Univ.ML	Fri Sep 15 11:34:46 2000 +0200
    30.2 +++ b/src/HOL/Univ.ML	Fri Sep 15 12:39:57 2000 +0200
    30.3 @@ -387,12 +387,8 @@
    30.4  by (Blast_tac 1);
    30.5  qed "Funs_mono";
    30.6  
    30.7 -val [p] = goalw (the_context ()) [Funs_def] "(!!x. f x : S) ==> f : Funs S";
    30.8 -by (rtac CollectI 1);
    30.9 -by (rtac subsetI 1);
   30.10 -by (etac rangeE 1);
   30.11 -by (etac ssubst 1);
   30.12 -by (rtac p 1);
   30.13 +val [prem] = Goalw [Funs_def] "(!!x. f x : S) ==> f : Funs S";
   30.14 +by (blast_tac (claset() addIs [prem]) 1);
   30.15  qed "FunsI";
   30.16  
   30.17  Goalw [Funs_def] "f : Funs S ==> f x : S";
   30.18 @@ -401,8 +397,8 @@
   30.19  by (rtac rangeI 1);
   30.20  qed "FunsD";
   30.21  
   30.22 -val [p1, p2] = goalw (the_context ()) [o_def]
   30.23 -  "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
   30.24 +val [p1, p2] = Goalw [o_def]
   30.25 +   "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
   30.26  by (rtac (p2 RS ext) 1);
   30.27  by (rtac (p1 RS FunsD) 1);
   30.28  qed "Funs_inv";
   30.29 @@ -412,7 +408,7 @@
   30.30  by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1);
   30.31  by (rtac ext 1);
   30.32  by (rtac (p1 RS FunsD RS rangeE) 1);
   30.33 -by (etac (exI RS (select_eq_Ex RS iffD2)) 1);
   30.34 +by (etac (exI RS (some_eq_ex RS iffD2)) 1);
   30.35  qed "Funs_rangeE";
   30.36  
   30.37  Goal "a : S ==> (%x. a) : Funs S";
    31.1 --- a/src/HOL/Vimage.ML	Fri Sep 15 11:34:46 2000 +0200
    31.2 +++ b/src/HOL/Vimage.ML	Fri Sep 15 12:39:57 2000 +0200
    31.3 @@ -77,11 +77,9 @@
    31.4  Addsimps [vimage_Collect_eq];
    31.5  
    31.6  (*A strange result used in Tools/inductive_package*)
    31.7 -bind_thm ("vimage_Collect", 
    31.8 -	  allI RS 
    31.9 -	  prove_goalw (the_context ()) [vimage_def]
   31.10 -	  "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
   31.11 -	      (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
   31.12 +val prems = Goal "(!!x. P (f x) = Q x) ==> f -`` (Collect P) = Collect Q";
   31.13 +by (force_tac (claset(), simpset() addsimps prems) 1);
   31.14 +qed "vimage_Collect";
   31.15  
   31.16  Addsimps [vimage_empty, vimage_Un, vimage_Int];
   31.17  
    32.1 --- a/src/HOL/WF_Rel.ML	Fri Sep 15 11:34:46 2000 +0200
    32.2 +++ b/src/HOL/WF_Rel.ML	Fri Sep 15 12:39:57 2000 +0200
    32.3 @@ -150,14 +150,14 @@
    32.4   by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
    32.5   by (rtac allI 1);
    32.6   by (Simp_tac 1);
    32.7 - by (rtac selectI2EX 1);
    32.8 + by (rtac someI2EX 1);
    32.9    by (Blast_tac 1);
   32.10   by (Blast_tac 1);
   32.11  by (rtac allI 1);
   32.12  by (induct_tac "n" 1);
   32.13   by (Asm_simp_tac 1);
   32.14  by (Simp_tac 1);
   32.15 -by (rtac selectI2EX 1);
   32.16 +by (rtac someI2EX 1);
   32.17   by (Blast_tac 1);
   32.18  by (Blast_tac 1);
   32.19  qed "wf_iff_no_infinite_down_chain";
    33.1 --- a/src/HOL/cladata.ML	Fri Sep 15 11:34:46 2000 +0200
    33.2 +++ b/src/HOL/cladata.ML	Fri Sep 15 12:39:57 2000 +0200
    33.3 @@ -59,7 +59,7 @@
    33.4                         addSEs [conjE,disjE,impCE,FalseE,iffCE];
    33.5  
    33.6  (*Quantifier rules*)
    33.7 -val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality] 
    33.8 +val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality] 
    33.9                       addSEs [exE] addEs [allE];
   33.10  
   33.11  val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];
    34.1 --- a/src/HOL/equalities.ML	Fri Sep 15 11:34:46 2000 +0200
    34.2 +++ b/src/HOL/equalities.ML	Fri Sep 15 12:39:57 2000 +0200
    34.3 @@ -104,8 +104,9 @@
    34.4  by (Blast_tac 1);
    34.5  qed "mk_disjoint_insert";
    34.6  
    34.7 -bind_thm ("insert_Collect", prove_goal (the_context ())
    34.8 -	  "insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
    34.9 +Goal "insert a (Collect P) = {u. u ~= a --> P u}";
   34.10 +by Auto_tac;
   34.11 +qed "insert_Collect";
   34.12  
   34.13  Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
   34.14  by (Blast_tac 1);
    35.1 --- a/src/HOL/ex/PiSets.ML	Fri Sep 15 11:34:46 2000 +0200
    35.2 +++ b/src/HOL/ex/PiSets.ML	Fri Sep 15 12:39:57 2000 +0200
    35.3 @@ -48,7 +48,7 @@
    35.4   by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 2);
    35.5    by (force_tac (claset(), simpset() addsimps [Graph_def]) 2);
    35.6   by (full_simp_tac (simpset() addsimps [Graph_def]) 2);
    35.7 -  by (stac select_equality 2);
    35.8 +  by (stac some_equality 2);
    35.9     by (assume_tac 2);
   35.10    by (Blast_tac 2);
   35.11   by (Blast_tac 2);
   35.12 @@ -56,7 +56,7 @@
   35.13  by (full_simp_tac (simpset() addsimps [PiBij_def,Graph_def]) 1);
   35.14  by (stac restrict_apply1 1);
   35.15   by (rtac restrictI 1);
   35.16 - by (blast_tac (claset() addSDs [[select_eq_Ex, ex1_implies_ex] MRS iffD2]) 1);
   35.17 + by (blast_tac (claset() addSDs [[some_eq_ex, ex1_implies_ex] MRS iffD2]) 1);
   35.18  (** LEVEL 17 **)
   35.19  by (rtac equalityI 1);
   35.20  by (rtac subsetI 1);
   35.21 @@ -65,11 +65,11 @@
   35.22  by (Blast_tac 2);
   35.23  by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
   35.24  (*Blast_tac: PROOF FAILED for depth 5*)
   35.25 -by (fast_tac (claset() addSIs [select1_equality RS sym]) 1);
   35.26 +by (fast_tac (claset() addSIs [some1_equality RS sym]) 1);
   35.27  (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
   35.28  by (Clarify_tac 1);
   35.29  by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
   35.30 -by (fast_tac (claset() addIs [selectI2]) 1);
   35.31 +by (fast_tac (claset() addIs [someI2]) 1);
   35.32  qed "surj_PiBij";
   35.33  
   35.34  Goal "f: Pi A B ==> \
    36.1 --- a/src/HOL/ex/Tarski.ML	Fri Sep 15 11:34:46 2000 +0200
    36.2 +++ b/src/HOL/ex/Tarski.ML	Fri Sep 15 12:39:57 2000 +0200
    36.3 @@ -273,7 +273,7 @@
    36.4  by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
    36.5  by (assume_tac 1);
    36.6  by (rewrite_goals_tac [lub_def,least_def]);
    36.7 -by (stac select_equality 1);
    36.8 +by (stac some_equality 1);
    36.9  by (rtac conjI 1);
   36.10  by (afs [islub_def] 2);
   36.11  by (etac conjunct2 2);
   36.12 @@ -290,7 +290,7 @@
   36.13  by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
   36.14  by (assume_tac 1);
   36.15  by (rewrite_goals_tac [lub_def,least_def]);
   36.16 -by (stac select_equality 1);
   36.17 +by (stac some_equality 1);
   36.18  by (rtac conjI 1);
   36.19  by (afs [islub_def] 2);
   36.20  by (etac conjunct2 2);
   36.21 @@ -315,7 +315,7 @@
   36.22  by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
   36.23  by (assume_tac 1);
   36.24  by (rewrite_goals_tac [lub_def,least_def]);
   36.25 -by (stac select_equality 1);
   36.26 +by (stac some_equality 1);
   36.27  by (afs [islub_def] 1);
   36.28  by (afs [islub_def, thm "A_def"] 2);
   36.29  by (rtac lub_unique 1);
   36.30 @@ -701,7 +701,7 @@
   36.31  
   36.32  Goal "Bot cl: A";
   36.33  by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1);
   36.34 -by (rtac selectI2 1);
   36.35 +by (rtac someI2 1);
   36.36  by (fold_goals_tac [thm "A_def"]);
   36.37  by (etac conjunct1 2);
   36.38  by (rtac conjI 1);
   36.39 @@ -719,7 +719,7 @@
   36.40  
   36.41  Goal "x: A ==> (x, Top cl): r";
   36.42  by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1);
   36.43 -by (rtac selectI2 1);
   36.44 +by (rtac someI2 1);
   36.45  by (fold_goals_tac [thm "r_def", thm "A_def"]);
   36.46  by (Fast_tac 2);
   36.47  by (rtac conjI 1);
    37.1 --- a/src/HOL/mono.ML	Fri Sep 15 11:34:46 2000 +0200
    37.2 +++ b/src/HOL/mono.ML	Fri Sep 15 12:39:57 2000 +0200
    37.3 @@ -109,9 +109,9 @@
    37.4    "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
    37.5  \  ==> (LEAST y. y : f``S) = f(LEAST x. x : S)";
    37.6  by (etac bexE 1);
    37.7 -by (rtac selectI2 1);
    37.8 +by (rtac someI2 1);
    37.9  by (Force_tac 1);
   37.10 -by (rtac select_equality 1);
   37.11 +by (rtac some_equality 1);
   37.12  by (Force_tac 1);
   37.13  by (force_tac (claset() addSIs [order_antisym], simpset()) 1);
   37.14  qed "Least_mono";
    38.1 --- a/src/HOL/simpdata.ML	Fri Sep 15 11:34:46 2000 +0200
    38.2 +++ b/src/HOL/simpdata.ML	Fri Sep 15 12:39:57 2000 +0200
    38.3 @@ -380,7 +380,7 @@
    38.4         if_True, if_False, if_cancel, if_eq_cancel,
    38.5         imp_disjL, conj_assoc, disj_assoc,
    38.6         de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
    38.7 -       disj_not1, not_all, not_ex, cases_simp, Eps_eq, Eps_sym_eq,
    38.8 +       disj_not1, not_all, not_ex, cases_simp, some_eq_trivial, some_sym_eq_trivial,
    38.9         thm"plus_ac0.zero", thm"plus_ac0_zero_right"]
   38.10       @ ex_simps @ all_simps @ simp_thms)
   38.11       addsimprocs [defALL_regroup,defEX_regroup]
    39.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Sep 15 11:34:46 2000 +0200
    39.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Sep 15 12:39:57 2000 +0200
    39.3 @@ -249,7 +249,7 @@
    39.4    by (etac ballE 1);
    39.5    by (Blast_tac 2);
    39.6    by (etac exE 1);
    39.7 -  by (rtac selectI2 1);
    39.8 +  by (rtac someI2 1);
    39.9    by (assume_tac 1);
   39.10    by (Blast_tac 1);
   39.11  qed"simulation_starts";
    40.1 --- a/src/HOLCF/Pcpo.ML	Fri Sep 15 11:34:46 2000 +0200
    40.2 +++ b/src/HOLCF/Pcpo.ML	Fri Sep 15 12:39:57 2000 +0200
    40.3 @@ -12,7 +12,7 @@
    40.4  (* ------------------------------------------------------------------------ *)
    40.5   
    40.6  Goalw [UU_def] "ALL z. UU << z";
    40.7 -by (rtac (select_eq_Ex RS iffD2) 1);
    40.8 +by (rtac (some_eq_ex RS iffD2) 1);
    40.9  by (rtac least 1);
   40.10  qed "UU_least";
   40.11  
    41.1 --- a/src/HOLCF/Porder0.ML	Fri Sep 15 11:34:46 2000 +0200
    41.2 +++ b/src/HOLCF/Porder0.ML	Fri Sep 15 12:39:57 2000 +0200
    41.3 @@ -12,7 +12,7 @@
    41.4  (* minimal fixes least element                                              *)
    41.5  (* ------------------------------------------------------------------------ *)
    41.6  Goal "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)";
    41.7 -by (blast_tac (claset() addIs [selectI2,antisym_less]) 1);
    41.8 +by (blast_tac (claset() addIs [someI2,antisym_less]) 1);
    41.9  bind_thm ("minimal2UU", allI RS result());
   41.10  
   41.11  (* ------------------------------------------------------------------------ *)
    42.1 --- a/src/HOLCF/Sprod0.ML	Fri Sep 15 11:34:46 2000 +0200
    42.2 +++ b/src/HOLCF/Sprod0.ML	Fri Sep 15 12:39:57 2000 +0200
    42.3 @@ -158,7 +158,7 @@
    42.4  (* ------------------------------------------------------------------------ *)
    42.5  
    42.6  Goalw [Isfst_def] "p=Ispair UU UU ==> Isfst p = UU";
    42.7 -by (rtac select_equality 1);
    42.8 +by (rtac some_equality 1);
    42.9  by (rtac conjI 1);
   42.10  by (fast_tac HOL_cs  1);
   42.11  by (strip_tac 1);
   42.12 @@ -187,7 +187,7 @@
   42.13  
   42.14  
   42.15  Goalw [Issnd_def] "p=Ispair UU UU ==>Issnd p=UU";
   42.16 -by (rtac select_equality 1);
   42.17 +by (rtac some_equality 1);
   42.18  by (rtac conjI 1);
   42.19  by (fast_tac HOL_cs  1);
   42.20  by (strip_tac 1);
   42.21 @@ -214,7 +214,7 @@
   42.22  Addsimps [strict_Issnd2];
   42.23  
   42.24  Goalw [Isfst_def] "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x";
   42.25 -by (rtac select_equality 1);
   42.26 +by (rtac some_equality 1);
   42.27  by (rtac conjI 1);
   42.28  by (strip_tac 1);
   42.29  by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
   42.30 @@ -230,7 +230,7 @@
   42.31  qed "Isfst";
   42.32  
   42.33  Goalw [Issnd_def] "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y";
   42.34 -by (rtac select_equality 1);
   42.35 +by (rtac some_equality 1);
   42.36  by (rtac conjI 1);
   42.37  by (strip_tac 1);
   42.38  by (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1);
    43.1 --- a/src/HOLCF/Ssum0.ML	Fri Sep 15 11:34:46 2000 +0200
    43.2 +++ b/src/HOLCF/Ssum0.ML	Fri Sep 15 12:39:57 2000 +0200
    43.3 @@ -223,7 +223,7 @@
    43.4  
    43.5  Goalw [Iwhen_def]
    43.6          "Iwhen f g (Isinl UU) = UU";
    43.7 -by (rtac select_equality 1);
    43.8 +by (rtac some_equality 1);
    43.9  by (rtac conjI 1);
   43.10  by (fast_tac HOL_cs  1);
   43.11  by (rtac conjI 1);
   43.12 @@ -246,7 +246,7 @@
   43.13  
   43.14  Goalw [Iwhen_def]
   43.15          "x~=UU ==> Iwhen f g (Isinl x) = f`x";
   43.16 -by (rtac select_equality 1);
   43.17 +by (rtac some_equality 1);
   43.18  by (fast_tac HOL_cs  2);
   43.19  by (rtac conjI 1);
   43.20  by (strip_tac 1);
   43.21 @@ -269,7 +269,7 @@
   43.22  
   43.23  Goalw [Iwhen_def]
   43.24          "y~=UU ==> Iwhen f g (Isinr y) = g`y";
   43.25 -by (rtac select_equality 1);
   43.26 +by (rtac some_equality 1);
   43.27  by (fast_tac HOL_cs  2);
   43.28  by (rtac conjI 1);
   43.29  by (strip_tac 1);
    44.1 --- a/src/HOLCF/Ssum1.ML	Fri Sep 15 11:34:46 2000 +0200
    44.2 +++ b/src/HOLCF/Ssum1.ML	Fri Sep 15 12:39:57 2000 +0200
    44.3 @@ -36,7 +36,7 @@
    44.4  
    44.5  Goalw [less_ssum_def]
    44.6  "[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)";
    44.7 -by (rtac select_equality 1);
    44.8 +by (rtac some_equality 1);
    44.9  by (dtac conjunct1 2);
   44.10  by (dtac spec 2);
   44.11  by (dtac spec 2);
   44.12 @@ -74,7 +74,7 @@
   44.13  
   44.14  Goalw [less_ssum_def]
   44.15  "[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)";
   44.16 -by (rtac select_equality 1);
   44.17 +by (rtac some_equality 1);
   44.18  by (dtac conjunct2 2);
   44.19  by (dtac conjunct1 2);
   44.20  by (dtac spec 2);
   44.21 @@ -113,7 +113,7 @@
   44.22  
   44.23  Goalw [less_ssum_def]
   44.24  "[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)";
   44.25 -by (rtac select_equality 1);
   44.26 +by (rtac some_equality 1);
   44.27  by (rtac conjI 1);
   44.28  by (strip_tac 1);
   44.29  by (etac conjE 1);
   44.30 @@ -152,7 +152,7 @@
   44.31  
   44.32  Goalw [less_ssum_def]
   44.33  "[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)";
   44.34 -by (rtac select_equality 1);
   44.35 +by (rtac some_equality 1);
   44.36  by (dtac conjunct2 2);
   44.37  by (dtac conjunct2 2);
   44.38  by (dtac conjunct2 2);