src/ZF/Sum.ML

--- a/src/ZF/Sum.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Sum.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -43,7 +43,7 @@
 val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
 
 goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Sigma_bool";
 
 (** Introduction rules for the injections **)
@@ -103,8 +103,6 @@
 
 Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
 
-val sum_cs = !claset;
-
 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
 by (Fast_tac 1);
 qed "InlD";
@@ -127,7 +125,7 @@
 qed "sum_equal_iff";
 
 goalw Sum.thy [sum_def] "A+A = 2*A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "sum_eq_2_times";
 
 
@@ -143,8 +141,6 @@
 
 Addsimps [case_Inl, case_Inr];
 
-val sum_ss = !simpset;
-
 val major::prems = goal Sum.thy
     "[| u: A+B; \
 \       !!x. x: A ==> c(x): C(Inl(x));   \
@@ -187,17 +183,17 @@
 qed "Part_mono";
 
 goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_Collect";
 
 bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
 
 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_Inl";
 
 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_Inr";
 
 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
@@ -205,13 +201,13 @@
 qed "PartD1";
 
 goal Sum.thy "Part(A,%x.x) = A";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_id";
 
 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_Inr2";
 
 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_sum_equality";