--- a/src/HOL/Sum.ML Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/Sum.ML Thu May 23 14:37:06 1996 +0200
@@ -56,12 +56,12 @@
val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "Inl_Rep_inject";
val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
qed "Inr_Rep_inject";
goalw Sum.thy [Inl_def] "inj(Inl)";
@@ -81,11 +81,11 @@
val Inr_inject = inj_Inr RS injD;
goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
-by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
+by (fast_tac (!claset addSEs [Inl_inject]) 1);
qed "Inl_eq";
goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
-by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
+by (fast_tac (!claset addSEs [Inr_inject]) 1);
qed "Inr_eq";
(*** Rules for the disjoint sum of two SETS ***)
@@ -117,15 +117,19 @@
addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
addSDs [Inl_inject, Inr_inject];
+AddSIs [InlI, InrI];
+AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl];
+AddSDs [Inl_inject, Inr_inject];
+
(** sum_case -- the selection operator for sums **)
goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
-by (fast_tac (sum_cs addIs [select_equality]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
qed "sum_case_Inl";
goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
-by (fast_tac (sum_cs addIs [select_equality]) 1);
+by (fast_tac (!claset addIs [select_equality]) 1);
qed "sum_case_Inr";
(** Exhaustion rule for sums -- a degenerate form of induction **)
@@ -151,10 +155,10 @@
by (rtac sumE 1);
by (etac ssubst 1);
by (stac sum_case_Inl 1);
-by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
+by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
by (etac ssubst 1);
by (stac sum_case_Inr 1);
-by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
+by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
qed "expand_sum_case";
Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, sum_case_Inl, sum_case_Inr];
@@ -171,7 +175,7 @@
goalw Sum.thy [Part_def]
"!!a b A h. [| a : A; a=h(b) |] ==> a : Part A h";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
qed "Part_eqI";
val PartI = refl RSN (2,Part_eqI);
@@ -190,7 +194,7 @@
qed "Part_subset";
goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
-by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
+by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
qed "Part_mono";
val basic_monos = basic_monos @ [Part_mono];
@@ -200,14 +204,14 @@
qed "PartD1";
goal Sum.thy "Part A (%x.x) = A";
-by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
qed "Part_id";
goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
-by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
qed "Part_Int";
(*For inductive definitions*)
goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
-by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
qed "Part_Collect";