--- a/src/HOL/Induct/LFilter.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/Induct/LFilter.ML Thu Jan 08 18:09:07 1998 +0100
@@ -69,12 +69,12 @@
(*** find: basic equations ***)
goalw thy [find_def] "find p LNil = LNil";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "find_LNil";
Addsimps [find_LNil];
goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
-by (blast_tac (claset() addIs [select_equality] addDs [findRel_functional]) 1);
+by (blast_tac (claset() addDs [findRel_functional]) 1);
qed "findRel_imp_find";
Addsimps [findRel_imp_find];
@@ -84,7 +84,7 @@
Addsimps [find_LCons_found];
goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "diverge_find_LNil";
Addsimps [diverge_find_LNil];
--- a/src/HOL/NatDef.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/NatDef.ML Thu Jan 08 18:09:07 1998 +0100
@@ -135,11 +135,11 @@
(*** nat_case -- the selection operator for nat ***)
goalw thy [nat_case_def] "nat_case a f 0 = a";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "nat_case_0";
goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "nat_case_Suc";
goalw thy [wf_def, pred_nat_def] "wf(pred_nat)";
--- a/src/HOL/Sexp.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/Sexp.ML Thu Jan 08 18:09:07 1998 +0100
@@ -11,15 +11,15 @@
(** sexp_case **)
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
-by (blast_tac (claset() addSIs [select_equality]) 1);
+by (Blast_tac 1);
qed "sexp_case_Leaf";
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
-by (blast_tac (claset() addSIs [select_equality]) 1);
+by (Blast_tac 1);
qed "sexp_case_Numb";
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
-by (blast_tac (claset() addSIs [select_equality]) 1);
+by (Blast_tac 1);
qed "sexp_case_Scons";
Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
--- a/src/HOL/Sum.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/Sum.ML Thu Jan 08 18:09:07 1998 +0100
@@ -119,11 +119,11 @@
(** sum_case -- the selection operator for sums **)
goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "sum_case_Inl";
goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "sum_case_Inr";
Addsimps [sum_case_Inl, sum_case_Inr];
--- a/src/HOL/Univ.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/Univ.ML Thu Jan 08 18:09:07 1998 +0100
@@ -432,15 +432,15 @@
(*** Split and Case ***)
goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "Split";
goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "Case_In0";
goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
-by (blast_tac (claset() addIs [select_equality]) 1);
+by (Blast_tac 1);
qed "Case_In1";
Addsimps [Split, Case_In0, Case_In1];
--- a/src/HOL/cladata.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOL/cladata.ML Thu Jan 08 18:09:07 1998 +0100
@@ -47,7 +47,7 @@
addSEs [conjE,disjE,impCE,FalseE,iffCE];
(*Quantifier rules*)
-val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]
+val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality]
addSEs [exE] addEs [allE];
claset_ref() := HOL_cs;
--- a/src/HOLCF/Sprod0.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOLCF/Sprod0.ML Thu Jan 08 18:09:07 1998 +0100
@@ -207,7 +207,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(rtac conjI 1),
(fast_tac HOL_cs 1),
(strip_tac 1),
@@ -242,7 +242,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(rtac conjI 1),
(fast_tac HOL_cs 1),
(strip_tac 1),
@@ -275,7 +275,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(rtac conjI 1),
(strip_tac 1),
(res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
@@ -295,7 +295,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(rtac conjI 1),
(strip_tac 1),
(res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
--- a/src/HOLCF/Ssum0.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOLCF/Ssum0.ML Thu Jan 08 18:09:07 1998 +0100
@@ -310,7 +310,7 @@
"Iwhen f g (Isinl UU) = UU"
(fn prems =>
[
- (rtac select_equality 1),
+ (rtac select_equality 1),
(rtac conjI 1),
(fast_tac HOL_cs 1),
(rtac conjI 1),
@@ -336,7 +336,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(fast_tac HOL_cs 2),
(rtac conjI 1),
(strip_tac 1),
@@ -362,7 +362,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(fast_tac HOL_cs 2),
(rtac conjI 1),
(strip_tac 1),
--- a/src/HOLCF/Ssum1.ML Thu Jan 08 18:08:43 1998 +0100
+++ b/src/HOLCF/Ssum1.ML Thu Jan 08 18:09:07 1998 +0100
@@ -45,7 +45,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(dtac conjunct1 2),
(dtac spec 2),
(dtac spec 2),
@@ -86,7 +86,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(dtac conjunct2 2),
(dtac conjunct1 2),
(dtac spec 2),
@@ -128,7 +128,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(rtac conjI 1),
(strip_tac 1),
(etac conjE 1),
@@ -170,7 +170,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac select_equality 1),
+ (rtac select_equality 1),
(dtac conjunct2 2),
(dtac conjunct2 2),
(dtac conjunct2 2),