# HG changeset patch
# User oheimb
# Date 884279347 -3600
# Node ID f24cebc299e4b28dca0522cf6e129eb482d449d2
# Parent  6932c3ae3912534fd898157ec983ec2fc0b020ba
added select_equality to the implicit claset

diff -r 6932c3ae3912 -r f24cebc299e4 src/HOL/Induct/LFilter.ML
--- 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];
 
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOL/NatDef.ML
--- 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)";
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOL/Sexp.ML
--- 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];
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOL/Sum.ML
--- 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];
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOL/Univ.ML
--- 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];
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOL/cladata.ML
--- 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;
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOLCF/Sprod0.ML
--- 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),
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOLCF/Ssum0.ML
--- 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),
diff -r 6932c3ae3912 -r f24cebc299e4 src/HOLCF/Ssum1.ML
--- 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),