--- 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
--- 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);
--- 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);
--- 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,
--- 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 |]\
--- 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)) ;
--- 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";
--- 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);
--- 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,
--- 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";
--- 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);
--- 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);
--- 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))";
--- 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)";
--- 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";
--- 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"
--- 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
--- 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
--- 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";
--- 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";
--- 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";
--- 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 ****)
--- 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]));
--- 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";
--- 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.*)
--- 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],
--- 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
--- 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 \
--- 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";
--- 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";
--- 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];
--- 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";
--- 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)];
--- 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);
--- 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 ==> \
--- 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);
--- 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";
--- 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]
--- 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";
--- 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";
--- 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());
(* ------------------------------------------------------------------------ *)
--- 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);
--- 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);
--- 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);