# HG changeset patch
# User paulson
# Date 852732267 -3600
# Node ID bdeb5024353af23079174b05f7c0e8bcab5ae014
# Parent  88f15198950f1960bf06cdf90eaea2fa33ec5e6c
Removal of sum_cs and eq_cs

diff -r 88f15198950f -r bdeb5024353a src/ZF/AC.ML
--- a/src/ZF/AC.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -14,7 +14,7 @@
 by (excluded_middle_tac "A=0" 1);
 by (asm_simp_tac (!simpset addsimps [Pi_empty1]) 2 THEN Fast_tac 2);
 (*The non-trivial case*)
-by (fast_tac (eq_cs addIs [AC, nonempty]) 1);
+by (fast_tac (!claset addIs [AC, nonempty]) 1);
 qed "AC_Pi";
 
 (*Using dtac, this has the advantage of DELETING the universal quantifier*)
@@ -27,7 +27,7 @@
 goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";
 by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
 by (etac exI 2);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "AC_Pi_Pow";
 
 val [nonempty] = goal AC.thy
@@ -40,7 +40,7 @@
 
 goal ZF.thy "!!x A. [| 0 ~: A;  x: A |] ==> EX y. y:x";
 by (subgoal_tac "x ~= 0" 1);
-by (ALLGOALS (fast_tac eq_cs));
+by (ALLGOALS (Fast_tac));
 qed "non_empty_family";
 
 goal AC.thy "!!A. 0 ~: A ==> EX f: A->Union(A). ALL x:A. f`x : x";
diff -r 88f15198950f -r bdeb5024353a src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -69,7 +69,7 @@
                setloop (split_tac [expand_if] ORELSE' etac UnE);
 
 goal upair.thy "{x, y} - {y} = {x} - {y}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 val double_Diff_sing = result();
 
 goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
diff -r 88f15198950f -r bdeb5024353a src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/DC.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -51,7 +51,7 @@
 by (rtac CollectI 1);
 by (rtac SigmaI 1);
 by (fast_tac (!claset addSIs [nat_0I RS UN_I, empty_fun]) 1);
-br (nat_1I RS UN_I) 1;
+by (rtac (nat_1I RS UN_I) 1);
 by (fast_tac (!claset addSIs [singleton_fun RS Pi_type]
         addss (!simpset addsimps [singleton_0 RS sym])) 1);
 by (asm_full_simp_tac (!simpset addsimps [domain_0, domain_cons,
@@ -115,9 +115,9 @@
 by (Step_tac 1);
 by (rtac bexI 1 THEN (assume_tac 2));
 by (best_tac (!claset addIs [ltD]
-		      addSEs [nat_0_le RS leE]
+                      addSEs [nat_0_le RS leE]
         addEs [sym RS trans RS succ_neq_0, domain_of_fun]
-	addss (!simpset)) 1);
+        addss (!simpset)) 1);
 (** LEVEL 7 **)
 by (dresolve_tac [nat_succI RSN (2, bspec)] 1 THEN (assume_tac 1));
 by (subgoal_tac "f ` succ(succ(x)) : succ(k)->X" 1);
@@ -276,7 +276,7 @@
 
 goal thy "!!x. x: X  \
 \ ==> {<0,x>}: (UN n:nat. {f:succ(n)->X. ALL k:n. <f`k, f`succ(k)> : R})";
-br (nat_0I RS UN_I) 1;
+by (rtac (nat_0I RS UN_I) 1);
 by (fast_tac (!claset addSIs [singleton_fun RS Pi_type]
         addss (!simpset addsimps [singleton_0 RS sym])) 1);
 val singleton_in_funs = result();
@@ -303,7 +303,7 @@
 by (step_tac (!claset delrules [domainE]) 1);
 by (swap_res_tac [bexI] 1 THEN etac singleton_in_funs 2);
 by (asm_full_simp_tac (!simpset addsimps [nat_0I  RSN (2, bexI), 
-				     cons_fun_type2, empty_fun]) 1);
+                                     cons_fun_type2, empty_fun]) 1);
 val lemma1 = result();
 
 goal thy "!!f. [| f:nat->X; n:nat |] ==>  \
@@ -392,8 +392,8 @@
 by (etac nat_induct 1);
 by (dresolve_tac [[nat_0I, Ord_nat] MRS ltI RSN (2, ospec)] 1);
 by (fast_tac (FOL_cs addss
-	      (!simpset addsimps [image_0, singleton_fun RS domain_of_fun,
-				  singleton_0, singleton_in_funs])) 1);
+              (!simpset addsimps [image_0, singleton_fun RS domain_of_fun,
+                                  singleton_0, singleton_in_funs])) 1);
 (*induction step*) (** LEVEL 5 **)
 by (Full_simp_tac 1);
 by (dresolve_tac [[nat_succI, Ord_nat] MRS ltI RSN (2, ospec)] 1
@@ -411,10 +411,10 @@
 by (etac domainE 1);
 
 by (forward_tac [f_n_type] 1 THEN REPEAT (assume_tac 1));
-br bexI 1;
+by (rtac bexI 1);
 by (etac nat_succI 2);
 by (res_inst_tac [("x","cons(<succ(xa), ya>, f`xa)")] bexI 1);
-br conjI 1;
+by (rtac conjI 1);
 by (fast_tac (FOL_cs
         addEs [subst_context RSN (2, trans) RS domain_cons_eq_succ,
         subst_context, all_in_image_restrict_eq, trans, equalityD1]) 2);
diff -r 88f15198950f -r bdeb5024353a src/ZF/AC/HH.ML
--- a/src/ZF/AC/HH.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/HH.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -149,7 +149,7 @@
 by (asm_full_simp_tac (!simpset addsimps [lam_type, Diff_eq_0_iff]) 1);
 by (Step_tac 1);
 by (set_mp_tac 1);
-by (deepen_tac (eq_cs addSIs [bexI] addSEs [equalityE]) 4 1);
+by (deepen_tac (!claset addSIs [bexI] addSEs [equalityE]) 4 1);
 val lam_surj_sing = result();
 
 goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0";
@@ -188,30 +188,32 @@
         addSDs [singleton_subsetD]) 1);
 val HH_subset_imp_eq = result();
 
-goal thy "!!f. [| f : (PROD X:Pow(x)-{0}. {{z}. z:x});  \
+goal thy "!!f. [| f : (Pow(x)-{0}) -> {{z}. z:x};  \
 \       a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}";
 by (dtac less_Least_subset_x 1);
 by (forward_tac [HH_subset_imp_eq] 1);
 by (dtac apply_type 1);
 by (resolve_tac [Diff_subset RS PowI RS DiffI] 1);
-by (fast_tac (!claset addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
-by (fast_tac (!claset addSEs [RepFunE] addEs [ssubst]) 1);
+by (fast_tac 
+    (!claset addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
+by (fast_tac (!claset addss (!simpset)) 1);
 val f_sing_imp_HH_sing = result();
 
 goalw thy [bij_def] 
         "!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0;  \
-\       f : (PROD X:Pow(x)-{0}. {{z}. z:x}) |]  \
+\       f : (Pow(x)-{0}) -> {{z}. z:x} |]  \
 \       ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a))  \
 \                       : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})";
 by (fast_tac (!claset addSIs [lam_Least_HH_inj, lam_surj_sing,
-                f_sing_imp_HH_sing]) 1);
+                              f_sing_imp_HH_sing]) 1);
 val f_sing_lam_bij = result();
 
 goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X))  \
 \       ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})";
 by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2]
-        addDs [apply_type]) 1);
+                     addDs [apply_type]) 1);
 val lam_singI = result();
 
-val bij_Least_HH_x = standard (lam_singI RSN (2, 
-        [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij] MRS comp_bij));
+val bij_Least_HH_x = 
+    (lam_singI RSN (2, [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij]
+                    MRS comp_bij)) |> standard;
diff -r 88f15198950f -r bdeb5024353a src/ZF/AC/WO1_WO8.ML
--- a/src/ZF/AC/WO1_WO8.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/WO1_WO8.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -24,7 +24,6 @@
 by (fast_tac (!claset addSEs [lam_sing_bij RS bij_is_inj RS
                         well_ord_rvimage]) 2);
 by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
-by (fast_tac (!claset addSEs [singleton_eq_iff RS iffD1 RS sym]
-                addSIs [lam_type]
-                addIs [the_equality RS ssubst]) 1);
+by (fast_tac (!claset addSIs [lam_type]
+                addss (!simpset addsimps [singleton_eq_iff, the_equality])) 1);
 qed "WO8_WO1";
diff -r 88f15198950f -r bdeb5024353a src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/WO2_AC16.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -124,7 +124,7 @@
 val Finite_lesspoll_infinite_Ord = result();
 
 goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 val Union_eq_Un_Diff = result();
 
 goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x))  \
@@ -182,7 +182,7 @@
 (* ********************************************************************** *)
 
 goal thy "A Un {a} = cons(a, A)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 val Un_sing_eq_cons = result();
 
 goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)";
@@ -361,7 +361,7 @@
 (* ********************************************************************** *)
 
 goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 val Diffs_eq_imp_eq = result();
 
 goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
@@ -538,27 +538,32 @@
 by (etac OUN_E 1);
 by (dtac prem1 1);
 by (Fast_tac 1);
+(** LEVEL 5 **)
 by (rtac ballI 1);
 by (etac imageE 1);
 by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS
         (prem3 RS Limit_has_succ)] 1);
 by (forward_tac [prem1] 1);
 by (etac conjE 1);
+(** LEVEL 10 **)
 by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1));
 by (etac impE 1);
 by (fast_tac (!claset addSEs [leI RS succ_leE RS lt_Ord RS le_refl]) 1);
 by (dresolve_tac [prem2 RSN (2, apply_equality)] 1);
 by (REPEAT (eresolve_tac [conjE, ex1E] 1));
+(** LEVEL 15 **)
 by (rtac ex1I 1);
 by (fast_tac (!claset addSIs [OUN_I]) 1);
 by (REPEAT (eresolve_tac [conjE, OUN_E] 1));
 by (eresolve_tac [lt_Ord RSN (2, lt_Ord RS Ord_linear_le)] 1 THEN (assume_tac 1));
 by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2));
-by (Fast_tac 2);
+(** LEVEL 20 **)
+by (fast_tac FOL_cs 2);
 by (forward_tac [prem1] 1);
 by (forward_tac [succ_leE] 1);
 by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1));
 by (etac conjE 1);
+(** LEVEL 25 **)
 by (dresolve_tac [lt_trans RSN (2, ospec)] 1 THEN (TRYALL assume_tac));
 by (dresolve_tac [disjI1 RSN (2, mp)] 1 THEN (assume_tac 1));
 by (etac ex1_two_eq 1);
@@ -573,7 +578,8 @@
         "!!n k. [| WO2; 0<m; k:nat; m:nat |] ==> AC16(k #+ m,k)";
 by (rtac allI 1);
 by (rtac impI 1);
-by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 THEN (REPEAT (assume_tac 1)));
+by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 
+    THEN (REPEAT (assume_tac 1)));
 by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1
         THEN (REPEAT (ares_tac [add_type] 1)));
 by (forward_tac [WO2_imp_ex_Card] 1);
diff -r 88f15198950f -r bdeb5024353a src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/WO6_WO1.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -65,7 +65,7 @@
 \            (EX b<a. f`b ~= 0 & (ALL g<a. ALL d<a. u(f,b,g,d) ~= 0 -->  \
 \                                       u(f,b,g,d) eqpoll m))";
 by (Asm_simp_tac 1);
-by (Fast_tac 1);
+by (fast_tac (!claset delrules [equalityI]) 1);
 val cases = result();
 
 (* ********************************************************************** *)
@@ -233,7 +233,7 @@
 \          |] ==> vv2(f,b,g,s) <= f`g";
 by (split_tac [expand_if] 1);
 by (Step_tac 1);
-be (uu_Least_is_fun RS apply_type) 1;
+by (etac (uu_Least_is_fun RS apply_type) 1);
 by (REPEAT_SOME (fast_tac (!claset addSIs [not_emptyI, singleton_subsetI])));
 val vv2_subset = result();
 
@@ -354,7 +354,7 @@
 goal thy "EX y. x Un y*y <= y";
 by (res_inst_tac [("x","UN n:nat. rec(n, x, %k r. r Un r*r)")] exI 1);
 by (safe_tac (!claset));
-br (nat_0I RS UN_I) 1;
+by (rtac (nat_0I RS UN_I) 1);
 by (Asm_simp_tac 1);
 by (res_inst_tac [("a","succ(n Un na)")] UN_I 1);
 by (eresolve_tac [Un_nat_type RS nat_succI] 1 THEN (assume_tac 1));
diff -r 88f15198950f -r bdeb5024353a src/ZF/AC/rel_is_fun.ML
--- a/src/ZF/AC/rel_is_fun.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/rel_is_fun.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -20,8 +20,8 @@
 by (etac domainE 1);
 by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
 by (rtac LeastI2 1);
-by (REPEAT (fast_tac (!claset addIs [fst_conv, left_inverse RS ssubst]
-                        addSEs [nat_into_Ord RS Ord_in_Ord]) 1));
+by (REPEAT (fast_tac (!claset addSEs [nat_into_Ord RS Ord_in_Ord]
+              addss (!simpset addsimps [left_inverse])) 1));
 val lepoll_m_imp_domain_lepoll_m = result();
 
 goalw Cardinal.thy [function_def]
diff -r 88f15198950f -r bdeb5024353a src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Arith.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -335,7 +335,7 @@
      nat_into_Ord, not_lt_iff_le RS iffD1];
 
 val div_ss = (!simpset) addsimps [nat_into_Ord, div_termination RS ltD,
-				  not_lt_iff_le RS iffD2];
+                                  not_lt_iff_le RS iffD2];
 
 (*Type checking depends upon termination!*)
 goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
@@ -585,7 +585,7 @@
 (*Thanks to Sten Agerholm*)
 goal Arith.thy  (* add_le_elim1 *)
     "!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
-be rev_mp 1;
+by (etac rev_mp 1);
 by (eres_inst_tac[("n","n")]nat_induct 1);
 by (Asm_simp_tac 1);
 by (Step_tac 1);
diff -r 88f15198950f -r bdeb5024353a src/ZF/Bool.ML
--- a/src/ZF/Bool.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Bool.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -11,7 +11,7 @@
 val bool_defs = [bool_def,cond_def];
 
 goalw Bool.thy [succ_def] "{0} = 1";
-br refl 1;
+by (rtac refl 1);
 qed "singleton_0";
 
 (* Introduction rules *)
diff -r 88f15198950f -r bdeb5024353a src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Cardinal.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -110,7 +110,7 @@
 qed "eqpoll_iff";
 
 goalw Cardinal.thy [lepoll_def, inj_def] "!!A. A lepoll 0 ==> A = 0";
-by (fast_tac (eq_cs addDs [apply_type]) 1);
+by (fast_tac (!claset addDs [apply_type]) 1);
 qed "lepoll_0_is_0";
 
 (*0 lepoll Y*)
@@ -163,7 +163,7 @@
                       addEs [apply_funtype RS succE]) 1);
 (*Proving it's injective*)
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
+by (fast_tac (!claset delrules [equalityI]) 1);
 qed "inj_not_surj_succ";
 
 (** Variations on transitivity **)
@@ -671,7 +671,7 @@
 by (forward_tac [Diff_sing_lepoll] 1);
 by (assume_tac 1);
 by (dtac lepoll_0_is_0 1);
-by (fast_tac (eq_cs addEs [equalityE]) 1);
+by (fast_tac (!claset addEs [equalityE]) 1);
 qed "lepoll_1_is_sing";
 
 goalw Cardinal.thy [lepoll_def] "A Un B lepoll A+B";
diff -r 88f15198950f -r bdeb5024353a src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/CardinalArith.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -421,7 +421,7 @@
 by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));
 by (REPEAT (etac ltE 1));
 by (asm_simp_tac (!simpset addsimps [rvimage_iff, rmult_iff, Memrel_iff,
-				     Un_absorb, Un_least_mem_iff, ltD]) 1);
+                                     Un_absorb, Un_least_mem_iff, ltD]) 1);
 qed "csquare_ltI";
 
 (*Part of the traditional proof.  UNUSED since it's harder to prove & apply *)
@@ -758,7 +758,7 @@
 by (subgoal_tac "cons(x,cons(xa,y)) = cons(xa,cons(x,y))" 1);
 by (Asm_simp_tac 1);
 by (fast_tac (!claset addSDs [cons_lepoll_consD]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Fin_imp_not_cons_lepoll";
 
 goal CardinalArith.thy
diff -r 88f15198950f -r bdeb5024353a src/ZF/Cardinal_AC.ML
--- a/src/ZF/Cardinal_AC.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Cardinal_AC.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -190,7 +190,7 @@
                      Card_is_Ord, Ord_0_lt_csucc]) 2);
 by (asm_full_simp_tac
     (!simpset addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
-by (safe_tac eq_cs);
+by (safe_tac (!claset addSIs [equalityI]));
 by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc] 
                   MRS lt_subset_trans] 1);
 by (REPEAT (assume_tac 1));
diff -r 88f15198950f -r bdeb5024353a src/ZF/Coind/MT.ML
--- a/src/ZF/Coind/MT.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Coind/MT.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -36,7 +36,7 @@
 AddDs [te_owrE,(ElabRel.dom_subset RS subsetD)];
 
 Addsimps [ve_dom_owr, te_dom_owr, ve_app_owr1, ve_app_owr2, 
-	  te_app_owr1, te_app_owr2];
+          te_app_owr1, te_app_owr2];
 
 val clean_tac = 
   REPEAT_FIRST (fn i => 
@@ -129,7 +129,7 @@
 by (etac htr_closE 1);
 by (etac elab_fnE 1);
 by (rewrite_tac Ty.con_defs);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (dtac (spec RS spec RS mp RS mp) 1);
 by (assume_tac 3);
 by (assume_tac 2);
diff -r 88f15198950f -r bdeb5024353a src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Coind/Map.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -11,19 +11,19 @@
 (* ############################################################ *)
 
 goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "qbeta";
 
 goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "qbeta_emp";
 
 goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "image_Sigma1";
 
 goal Map.thy "0``A = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "image_02";
 
 (* ############################################################ *)
@@ -107,7 +107,7 @@
 
 goalw Map.thy [TMap_def,map_app_def,domain_def] 
   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "tmap_appI";
 
 goalw Map.thy [PMap_def]
@@ -123,12 +123,12 @@
 
 goalw Map.thy [TMap_def]
   "!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "tmap_domainD";
 
 goalw Map.thy [PMap_def,TMap_def]
   "!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "pmap_domainD";
 
 (* ############################################################ *)
@@ -140,33 +140,33 @@
 (* Lemmas *)
 
 goal Map.thy  "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_UN";
 
 goal Map.thy  "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
 by (simp_tac (!simpset addsimps [domain_UN,domain_0,domain_cons]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_Sigma";
 
 (* Theorems *)
 
 goalw Map.thy [map_emp_def] "domain(map_emp) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "map_domain_emp";
 
 goalw Map.thy [map_owr_def] 
   "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
 by (simp_tac (!simpset addsimps [domain_Sigma]) 1);
 by (rtac equalityI 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 by (rtac subsetI 1);
 by (rtac CollectI 1);
 by (assume_tac 1);
 by (etac UnE' 1);
 by (etac singletonE 1);
 by (Asm_simp_tac 1);
-by (fast_tac eq_cs 1);
-by (fast_tac (eq_cs addss (!simpset)) 1);
+by (Fast_tac 1);
+by (fast_tac (!claset addss (!simpset)) 1);
 qed "map_domain_owr";
 
 (** Application **)
@@ -183,7 +183,7 @@
 by (rtac (excluded_middle RS disjE) 1);
 by (stac qbeta_emp 1);
 by (assume_tac 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 by (etac (qbeta RS ssubst) 1);
 by (Asm_simp_tac 1);
 qed "map_app_owr2";
diff -r 88f15198950f -r bdeb5024353a src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Epsilon.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -112,7 +112,7 @@
 
 goalw Epsilon.thy [Transset_def]
     "!!i j. [| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j";
-by (fast_tac (eq_cs addSIs [MemrelI] addSEs [MemrelE]) 1);
+by (fast_tac (!claset addSIs [MemrelI] addSEs [MemrelE]) 1);
 qed "under_Memrel";
 
 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
diff -r 88f15198950f -r bdeb5024353a src/ZF/EquivClass.ML
--- a/src/ZF/EquivClass.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/EquivClass.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -110,7 +110,7 @@
 
 goalw EquivClass.thy [equiv_def,refl_def,quotient_def]
     "!!A r. equiv(A,r) ==> Union(A/r) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Union_quotient";
 
 goalw EquivClass.thy [quotient_def]
@@ -181,7 +181,7 @@
 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
-				     congruent2_implies_congruent]) 1);
+                                     congruent2_implies_congruent]) 1);
 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
 by (Fast_tac 1);
 qed "congruent2_implies_congruent_UN";
@@ -191,8 +191,8 @@
 \    ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
 by (cut_facts_tac prems 1);
 by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
-				     congruent2_implies_congruent,
-				     congruent2_implies_congruent_UN]) 1);
+                                     congruent2_implies_congruent,
+                                     congruent2_implies_congruent_UN]) 1);
 qed "UN_equiv_class2";
 
 (*type checking*)
@@ -249,6 +249,6 @@
 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [commute,
-				     [equivA, congt] MRS UN_equiv_class]) 1);
+                                     [equivA, congt] MRS UN_equiv_class]) 1);
 by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
 qed "congruent_commuteI";
diff -r 88f15198950f -r bdeb5024353a src/ZF/List.ML
--- a/src/ZF/List.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/List.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -28,7 +28,7 @@
 
 goal List.thy "list(A) = {0} + (A * list(A))";
 let open list;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "list_unfold";
@@ -113,7 +113,7 @@
 
 goalw List.thy [drop_def]
     "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
-br sym 1;
+by (rtac sym 1);
 by (etac nat_induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
diff -r 88f15198950f -r bdeb5024353a src/ZF/Order.ML
--- a/src/ZF/Order.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Order.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -82,13 +82,13 @@
 
 goalw Order.thy [pred_def]
     "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "pred_pred_eq";
 
 goalw Order.thy [trans_on_def, pred_def]
     "!!r. [| trans[A](r);  <y,x>:r;  x:A;  y:A \
 \         |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "trans_pred_pred_eq";
 
 
@@ -171,7 +171,7 @@
 qed "tot_ord_0";
 
 goalw Order.thy [wf_on_def, wf_def] "wf[0](r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "wf_on_0";
 
 goalw Order.thy [well_ord_def] "well_ord(0,r)";
@@ -300,7 +300,7 @@
 goalw Order.thy [part_ord_def, irrefl_def, trans_on_def, ord_iso_def]
     "!!A B r. [| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)";
 by (Asm_simp_tac 1);
-by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1);
+by (fast_tac (!claset addIs [bij_is_fun RS apply_type]) 1);
 qed "part_ord_ord_iso";
 
 goalw Order.thy [linear_def, ord_iso_def]
@@ -319,11 +319,10 @@
 by (asm_full_simp_tac (!simpset addcongs [conj_cong2]) 1);
 by (safe_tac (!claset));
 by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
-by (safe_tac eq_cs);
+by (safe_tac (!claset addSIs [equalityI]));
 by (dtac equalityD1 1);
 by (fast_tac (!claset addSIs [bexI]) 1);
-by (fast_tac (!claset addSIs [bexI]
-              addIs [bij_is_fun RS apply_type]) 1);
+by (fast_tac (!claset addSIs [bexI] addIs [bij_is_fun RS apply_type]) 1);
 qed "wf_on_ord_iso";
 
 goalw Order.thy [well_ord_def, tot_ord_def]
@@ -382,7 +381,8 @@
 by (etac CollectE 1);
 by (asm_simp_tac 
     (!simpset addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
-by (safe_tac (eq_cs addSEs [bij_is_fun RS apply_type]));
+by (rtac equalityI 1);
+by (safe_tac (!claset addSEs [bij_is_fun RS apply_type]));
 by (rtac RepFun_eqI 1);
 by (fast_tac (!claset addSIs [right_inverse_bij RS sym]) 1);
 by (asm_simp_tac bij_inverse_ss 1);
@@ -472,7 +472,7 @@
 
 goalw Order.thy [ord_iso_map_def]
     "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
-by (fast_tac (eq_cs addIs [ord_iso_sym]) 1);
+by (fast_tac (!claset addIs [ord_iso_sym]) 1);
 qed "converse_ord_iso_map";
 
 goalw Order.thy [ord_iso_map_def, function_def]
diff -r 88f15198950f -r bdeb5024353a src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/OrderArith.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -15,22 +15,22 @@
 
 goalw OrderArith.thy [radd_def] 
     "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "radd_Inl_Inr_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "radd_Inl_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "radd_Inr_iff";
 
 goalw OrderArith.thy [radd_def] 
     "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "radd_Inr_Inl_iff";
 
 (** Elimination Rule **)
@@ -48,7 +48,7 @@
 (*Apply each premise to correct subgoal; can't just use fast_tac
   because hyp_subst_tac would delete equalities too quickly*)
 by (EVERY (map (fn prem => 
-                EVERY1 [rtac prem, assume_tac, REPEAT o fast_tac sum_cs])
+                EVERY1 [rtac prem, assume_tac, REPEAT o Fast_tac])
            prems));
 qed "raddE";
 
@@ -63,7 +63,7 @@
 (** Linearity **)
 
 Addsimps [radd_Inl_iff, radd_Inr_iff, 
-	  radd_Inl_Inr_iff, radd_Inr_Inl_iff];
+          radd_Inl_Inr_iff, radd_Inr_Inl_iff];
 
 goalw OrderArith.thy [linear_def]
     "!!r s. [| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
@@ -83,15 +83,15 @@
 by (rtac ballI 2);
 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
 by (etac (bspec RS mp) 2);
-by (fast_tac sum_cs 2);
-by (best_tac (sum_cs addSEs [raddE]) 2);
+by (Fast_tac 2);
+by (best_tac (!claset addSEs [raddE]) 2);
 (*Returning to main part of proof*)
 by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
-by (best_tac sum_cs 1);
+by (Best_tac 1);
 by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
 by (etac (bspec RS mp) 1);
-by (fast_tac sum_cs 1);
-by (best_tac (sum_cs addSEs [raddE]) 1);
+by (Fast_tac 1);
+by (best_tac (!claset addSEs [raddE]) 1);
 qed "wf_on_radd";
 
 goal OrderArith.thy
@@ -129,7 +129,7 @@
 by (safe_tac (!claset addSIs [sum_bij]));
 (*Do the beta-reductions now*)
 by (ALLGOALS (Asm_full_simp_tac));
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 (*8 subgoals!*)
 by (ALLGOALS
     (asm_full_simp_tac 
@@ -143,9 +143,9 @@
 \           (lam z:A+B. case(%x.x, %y.y, z)) : bij(A+B, A Un B)";
 by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")] 
     lam_bijective 1);
-by (fast_tac (sum_cs addSIs [if_type]) 2);
+by (fast_tac (!claset addSIs [if_type]) 2);
 by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1));
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
 by (fast_tac (!claset addEs [equalityE]) 1);
 qed "sum_disjoint_bij";
@@ -295,10 +295,10 @@
 by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
 by (rtac singleton_prod_bij 1);
 by (rtac sum_disjoint_bij 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [case_cong] addsimps [id_conv]) 1);
 by (resolve_tac [comp_lam RS trans RS sym] 1);
-by (fast_tac (sum_cs addSEs [case_type]) 1);
+by (fast_tac (!claset addSEs [case_type]) 1);
 by (asm_simp_tac (!simpset addsimps [case_case]) 1);
 qed "prod_sum_singleton_bij";
 
@@ -374,7 +374,7 @@
 
 goalw OrderArith.thy [rvimage_def] 
     "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "rvimage_converse";
 
 
@@ -441,5 +441,5 @@
 
 goalw OrderArith.thy [ord_iso_def, rvimage_def]
     "!!A B. f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "ord_iso_rvimage_eq";
diff -r 88f15198950f -r bdeb5024353a src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/OrderType.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -32,12 +32,12 @@
 goalw OrderType.thy [pred_def, lt_def]
     "!!i j. j<i ==> pred(i, j, Memrel(i)) = j";
 by (asm_simp_tac (!simpset addsimps [Memrel_iff]) 1);
-by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+by (fast_tac (!claset addEs [Ord_trans]) 1);
 qed "lt_pred_Memrel";
 
 goalw OrderType.thy [pred_def,Memrel_def] 
       "!!A x. x:A ==> pred(A, x, Memrel(A)) = A Int x";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "pred_Memrel";
 
 goal OrderType.thy
@@ -241,7 +241,7 @@
 by (asm_full_simp_tac (!simpset addsimps [pred_def]) 1);
 by (rtac (refl RSN (2,RepFun_cong)) 1);
 by (dtac well_ord_is_trans_on 1);
-by (fast_tac (eq_cs addSEs [trans_onD]) 1);
+by (fast_tac (!claset addSEs [trans_onD]) 1);
 qed "ordermap_pred_eq_ordermap";
 
 goalw OrderType.thy [ordertype_def]
@@ -275,7 +275,8 @@
 goal OrderType.thy
     "!!A r. well_ord(A,r) ==>  \
 \           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
-by (safe_tac (eq_cs addSIs [ordertype_pred_lt RS ltD]));
+by (rtac equalityI 1);
+by (safe_tac (!claset addSIs [ordertype_pred_lt RS ltD]));
 by (fast_tac
     (!claset addss
      (!simpset addsimps [ordertype_def, 
@@ -294,7 +295,7 @@
 by (rtac conjI 1);
 by (etac well_ord_Memrel 1);
 by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Ord_is_Ord_alt";
 
 (*proof by lcp*)
@@ -319,7 +320,7 @@
 
 goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
 by (res_inst_tac [("d", "Inl")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (Asm_simp_tac));
 qed "bij_sum_0";
 
@@ -327,12 +328,12 @@
  "!!A r. well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
 by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
 by (assume_tac 2);
-by (fast_tac (sum_cs addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
 qed "ordertype_sum_0_eq";
 
 goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
 by (res_inst_tac [("d", "Inr")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (Asm_simp_tac));
 qed "bij_0_sum";
 
@@ -340,7 +341,7 @@
  "!!A r. well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
 by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
 by (assume_tac 2);
-by (fast_tac (sum_cs addss (!simpset addsimps [radd_Inr_iff, Memrel_iff])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [radd_Inr_iff, Memrel_iff])) 1);
 qed "ordertype_0_sum_eq";
 
 (** Initial segments of radd.  Statements by Grabczewski **)
@@ -351,7 +352,7 @@
 \        (lam x:pred(A,a,r). Inl(x))    \
 \        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS
     (asm_full_simp_tac 
      (!simpset addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
@@ -371,7 +372,7 @@
 \        id(A+pred(B,b,s))      \
 \        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
 by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
-by (safe_tac sum_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (Asm_full_simp_tac));
 qed "pred_Inr_bij";
 
@@ -380,7 +381,7 @@
 \        ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
 \        ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
 by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (fast_tac (sum_cs addss (!simpset addsimps [pred_def, id_def])) 2);
+by (fast_tac (!claset addss (!simpset addsimps [pred_def, id_def])) 2);
 by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset]));
 qed "ordertype_pred_Inr_eq";
 
@@ -414,9 +415,9 @@
 by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
 by (asm_simp_tac 
     (!simpset addsimps [ordertype_pred_unfold, 
-			well_ord_radd, well_ord_Memrel,
-			ordertype_pred_Inl_eq, 
-			lt_pred_Memrel, leI RS le_ordertype_Memrel]
+                        well_ord_radd, well_ord_Memrel,
+                        ordertype_pred_Inl_eq, 
+                        lt_pred_Memrel, leI RS le_ordertype_Memrel]
            setloop rtac (InlI RSN (2,bexI))) 1);
 qed "lt_oadd1";
 
@@ -487,7 +488,7 @@
     (!simpset addsimps [ordertype_pred_unfold, well_ord_radd,
                      well_ord_Memrel]) 1);
 by (eresolve_tac [ltD RS RepFunE] 1);
-by (fast_tac (sum_cs addss 
+by (fast_tac (!claset addss 
               (!simpset addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
                                ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
                                ordertype_pred_Inr_eq, 
@@ -522,12 +523,12 @@
 
 goal OrderType.thy "!!i. Ord(i) ==> i++1 = succ(i)";
 by (asm_simp_tac (!simpset addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "oadd_1";
 
 goal OrderType.thy
     "!!i. [| Ord(i);  Ord(j) |] ==> i++succ(j) = succ(i++j)";
-		(*ZF_ss prevents looping*)
+                (*ZF_ss prevents looping*)
 by (asm_simp_tac (ZF_ss addsimps [Ord_oadd, oadd_1 RS sym]) 1);
 by (asm_simp_tac (!simpset addsimps [oadd_1, oadd_assoc, Ord_1]) 1);
 qed "oadd_succ";
@@ -538,7 +539,7 @@
 val prems = goal OrderType.thy
     "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
 \    i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (fast_tac (eq_cs addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
+by (fast_tac (!claset addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
                                     lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
                      addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
 qed "oadd_UN";
@@ -562,7 +563,7 @@
 by (rtac le_implies_UN_le_UN 2);
 by (Fast_tac 2);
 by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
-				     le_refl, Limit_is_Ord]) 1);
+                                     le_refl, Limit_is_Ord]) 1);
 qed "oadd_le_self2";
 
 goal OrderType.thy "!!i j k. [| k le j;  Ord(i) |] ==> k++i le j++i";
@@ -600,7 +601,7 @@
 goal OrderType.thy
     "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
 by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
-by (fast_tac (sum_cs addSIs [if_type]) 1);
+by (fast_tac (!claset addSIs [if_type]) 1);
 by (fast_tac (!claset addSIs [case_type]) 1);
 by (etac sumE 2);
 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
@@ -677,7 +678,8 @@
  "!!A B. [| a:A;  b:B |] ==>  \
 \        pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
 \        pred(A,a,r)*B Un ({a} * pred(B,b,s))";
-by (safe_tac eq_cs);
+by (rtac equalityI 1);
+by (safe_tac (!claset));
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [rmult_iff])));
 by (ALLGOALS (Fast_tac));
 qed "pred_Pair_eq";
@@ -730,7 +732,7 @@
 by (rtac ltI 1);
 by (asm_simp_tac
     (!simpset addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
-			lt_Ord2]) 2);
+                        lt_Ord2]) 2);
 by (asm_simp_tac 
     (!simpset addsimps [ordertype_pred_unfold, 
                      well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
@@ -738,7 +740,7 @@
 by (fast_tac (!claset addSEs [ltE]) 2);
 by (asm_simp_tac 
     (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
-			symmetric omult_def]) 1);
+                        symmetric omult_def]) 1);
 qed "omult_oadd_lt";
 
 goal OrderType.thy
@@ -802,7 +804,7 @@
 qed "oadd_omult_distrib";
 
 goal OrderType.thy "!!i. [| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
-		(*ZF_ss prevents looping*)
+                (*ZF_ss prevents looping*)
 by (asm_simp_tac (ZF_ss addsimps [oadd_1 RS sym]) 1);
 by (asm_simp_tac 
     (!simpset addsimps [omult_1, oadd_omult_distrib, Ord_1]) 1);
@@ -830,7 +832,7 @@
     "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
 \    i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
 by (asm_simp_tac (!simpset addsimps (prems@[Ord_UN, omult_unfold])) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "omult_UN";
 
 goal OrderType.thy 
@@ -909,7 +911,7 @@
 by (rtac le_implies_UN_le_UN 2);
 by (Fast_tac 2);
 by (asm_simp_tac (!simpset addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
-				     Limit_is_Ord RS le_refl]) 1);
+                                     Limit_is_Ord RS le_refl]) 1);
 qed "omult_le_self2";
 
 
diff -r 88f15198950f -r bdeb5024353a src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Ordinal.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -17,7 +17,7 @@
 qed "Transset_iff_Pow";
 
 goalw Ordinal.thy [Transset_def] "Transset(A) <-> Union(succ(A)) = A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "Transset_iff_Union_succ";
 
 (** Consequences of downwards closure **)
@@ -314,11 +314,11 @@
 qed "Memrel_mono";
 
 goalw Ordinal.thy [Memrel_def] "Memrel(0) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Memrel_0";
 
 goalw Ordinal.thy [Memrel_def] "Memrel(1) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Memrel_1";
 
 Addsimps [Memrel_0, Memrel_1];
@@ -396,7 +396,7 @@
 by (trans_ind_tac "i" prems 1);
 by (rtac (impI RS allI) 1);
 by (trans_ind_tac "j" [] 1);
-by (DEPTH_SOLVE (step_tac eq_cs 1 ORELSE Ord_trans_tac 1));
+by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1));
 qed "Ord_linear_lemma";
 
 (*"[| Ord(i); Ord(x) |] ==> i:x | i=x | x:i"*)
@@ -623,7 +623,7 @@
 qed "le_implies_UN_le_UN";
 
 goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
-by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+by (fast_tac (!claset addEs [Ord_trans]) 1);
 qed "Ord_equality";
 
 (*Holds for all transitive sets, not just ordinals*)
@@ -635,7 +635,7 @@
 (*** Limit ordinals -- general properties ***)
 
 goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Union(i) = i";
-by (fast_tac (eq_cs addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
+by (fast_tac (!claset addSIs [ltI] addSEs [ltE] addEs [Ord_trans]) 1);
 qed "Limit_Union_eq";
 
 goalw Ordinal.thy [Limit_def] "!!i. Limit(i) ==> Ord(i)";
@@ -673,7 +673,7 @@
 
 goal Ordinal.thy "!!i. Ord(i) ==> i=0 | (EX j. Ord(j) & i=succ(j)) | Limit(i)";
 by (fast_tac (!claset addSIs [non_succ_LimitI, Ord_0_lt]
-         	      addSDs [Ord_succD]) 1);
+                      addSDs [Ord_succD]) 1);
 qed "Ord_cases_disj";
 
 val major::prems = goal Ordinal.thy
diff -r 88f15198950f -r bdeb5024353a src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Perm.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -23,7 +23,7 @@
 qed "fun_is_surj";
 
 goalw Perm.thy [surj_def] "!!f A B. f: surj(A,B) ==> range(f)=B";
-by (best_tac (!claset addIs [equalityI,apply_Pair] addEs [range_type]) 1);
+by (best_tac (!claset addIs [apply_Pair] addEs [range_type]) 1);
 qed "surj_range";
 
 (** A function with a right inverse is a surjection **)
@@ -269,7 +269,7 @@
 qed "domain_comp_eq";
 
 goal Perm.thy "(r O s)``A = r``(s``A)";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "image_comp";
 
 
@@ -286,21 +286,21 @@
 
 (*associative law for composition*)
 goal Perm.thy "(r O s) O t = r O (s O t)";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "comp_assoc";
 
 (*left identity of composition; provable inclusions are
         id(A) O r <= r       
   and   [| r<=A*B; B<=C |] ==> r <= id(C) O r *)
 goal Perm.thy "!!r A B. r<=A*B ==> id(B) O r = r";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "left_comp_id";
 
 (*right identity of composition; provable inclusions are
         r O id(A) <= r
   and   [| r<=A*B; A<=C |] ==> r <= r O id(C) *)
 goal Perm.thy "!!r A B. r<=A*B ==> r O id(A) = r";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "right_comp_id";
 
 
@@ -404,7 +404,7 @@
 (*left inverse of composition; one inclusion is
         f: A->B ==> id(A) <= converse(f) O f *)
 goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) O f = id(A)";
-by (fast_tac (!claset addIs [equalityI, apply_Pair] 
+by (fast_tac (!claset addIs [apply_Pair] 
                       addEs [domain_type]
                addss (!simpset addsimps [apply_iff])) 1);
 qed "left_comp_inverse";
diff -r 88f15198950f -r bdeb5024353a src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/QPair.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -88,10 +88,10 @@
  (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
 
 qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "QSigma_empty2" thy "A <*> 0 = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 Addsimps [QSigma_empty1, QSigma_empty2];
 
@@ -192,17 +192,17 @@
 
 qed_goal "qconverse_qconverse" thy
     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "qconverse_type" thy
     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
  (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "qconverse_prod" thy "qconverse(A <*> B) = B <*> A"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "qconverse_empty" thy "qconverse(0) = 0"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 
 (**** The Quine-inspired notion of disjoint sum ****)
@@ -315,17 +315,17 @@
 (** Rules for the Part primitive **)
 
 goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_QInl";
 
 goal thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_QInr";
 
 goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_QInr2";
 
 goal thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "Part_qsum_equality";
diff -r 88f15198950f -r bdeb5024353a src/ZF/Resid/Cube.ML
--- a/src/ZF/Resid/Cube.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Resid/Cube.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -74,10 +74,10 @@
 
 goal Cube.thy 
     "!!u.[|w~u; w~v; regular(u); regular(v)|]==> \
-\          EX uv.EX vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
+\          EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
 \            regular(vu) & (w|>v)~uv & regular(uv) ";
 by (forw_inst_tac [("x1","v")] (comp_sym RS comp_trans) 1);
-by (REPEAT(Step_tac 1));
+by (step_tac (!claset addSIs [exI]) 1);
 by (rtac cube 1);
 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
 by (asm_simp_tac (prism_ss addsimps [comp_sym_iff]) 1);
diff -r 88f15198950f -r bdeb5024353a 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";
diff -r 88f15198950f -r bdeb5024353a src/ZF/Trancl.ML
--- a/src/ZF/Trancl.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Trancl.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -55,7 +55,7 @@
 qed "r_subset_rtrancl";
 
 goal Trancl.thy "field(r^*) = field(r)";
-by (fast_tac (eq_cs addIs [r_into_rtrancl] 
+by (fast_tac (!claset addIs [r_into_rtrancl] 
                     addSDs [rtrancl_type RS subsetD]) 1);
 qed "rtrancl_field";
 
diff -r 88f15198950f -r bdeb5024353a src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Univ.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -122,7 +122,7 @@
 
 goal Univ.thy "Vfrom(A,0) = A";
 by (stac Vfrom 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Vfrom_0";
 
 goal Univ.thy "!!i. Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
@@ -258,7 +258,7 @@
 qed "Inr_in_VLimit";
 
 goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)";
-by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
+by (fast_tac (!claset addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1);
 qed "sum_VLimit";
 
 bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans);
@@ -284,7 +284,7 @@
 
 goalw Ordinal.thy [Pair_def,Transset_def]
     "!!C. [| <a,b> <= C; Transset(C) |] ==> a: C & b: C";
-by (Fast_tac 1);
+by (Best_tac 1);
 qed "Transset_Pair_subset";
 
 goal Univ.thy
@@ -387,7 +387,7 @@
 
 goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
 by (stac Vfrom 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Vset";
 
 val Vset_succ = Transset_0 RS Transset_Vfrom_succ;
diff -r 88f15198950f -r bdeb5024353a src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ZF.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -152,6 +152,8 @@
 qed_goal "equalityI" ZF.thy "[| A <= B;  B <= A |] ==> A = B"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
 
+AddIs [equalityI];
+
 qed_goal "equality_iffI" ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
  (fn [prem] =>
   [ (rtac equalityI 1),
@@ -268,7 +270,7 @@
  (fn _ => [Fast_tac 1]);
 
 goal ZF.thy "{x.x:A} = A";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (fast_tac (!claset) 1);
 qed "triv_RepFun";
 
 Addsimps [RepFun_iff, triv_RepFun];
@@ -438,7 +440,7 @@
 AddSIs [empty_subsetI];
 
 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
- (fn prems=> [ fast_tac (!claset addIs [equalityI] addDs prems) 1 ]);
+ (fn prems=> [ fast_tac (!claset addDs prems) 1 ]);
 
 qed_goal "equals0D" ZF.thy "!!P. [| A=0;  a:A |] ==> P"
  (fn _=> [ Full_simp_tac 1, Fast_tac 1 ]);
diff -r 88f15198950f -r bdeb5024353a src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/Zorn.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -281,7 +281,7 @@
 by (subgoal_tac "cons(z,c): super(S,c)" 1);
 by (fast_tac (!claset addEs [equalityE]) 1);
 by (rewtac super_def);
-by (safe_tac eq_cs);
+by (safe_tac (!claset));
 by (fast_tac (!claset addEs [chain_extend]) 1);
 by (best_tac (!claset addEs [equalityE]) 1);
 qed "Zorn";
@@ -301,7 +301,7 @@
 by (REPEAT_SOME (eresolve_tac [asm_rl,subsetD]));
 by (subgoal_tac "x = Inter(Z)" 1);
 by (Fast_tac 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "TFin_well_lemma5";
 
 (*Well-ordering of TFin(S,next)*)
@@ -334,7 +334,7 @@
 by (rtac wf_onI 1);
 by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1);
 by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "well_ord_TFin";
 
 (** Defining the "next" operation for Zermelo's Theorem **)
@@ -343,7 +343,7 @@
     "!!S. [| ch : (PROD X:Pow(S) - {0}. X);  X<=S;  X~=S        \
 \         |] ==> ch ` (S-X) : S-X";
 by (etac apply_type 1);
-by (fast_tac (eq_cs addEs [equalityE]) 1);
+by (fast_tac (!claset addEs [equalityE]) 1);
 qed "choice_Diff";
 
 (*This justifies Definition 6.1*)
@@ -392,7 +392,7 @@
 \                  Union({y: TFin(S,next). x~: y})" 1);
 by (asm_simp_tac 
     (!simpset delsimps [Union_iff]
-	      addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
+              addsimps [Collect_subset RS TFin_UnionI RS TFin_is_subset,
                      Pow_iff, cons_subset_iff, subset_refl,
                      choice_Diff RS DiffD2]
            setloop split_tac [expand_if]) 2);
diff -r 88f15198950f -r bdeb5024353a src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/domrange.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -36,16 +36,16 @@
 
 qed_goal "converse_converse" thy
     "!!A B r. r<=Sigma(A,B) ==> converse(converse(r)) = r"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "converse_type" thy "!!A B r. r<=A*B ==> converse(r)<=B*A"
  (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "converse_prod" thy "converse(A*B) = B*A"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "converse_empty" thy "converse(0) = 0"
- (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 Addsimps [converse_prod, converse_empty];
 
@@ -191,9 +191,7 @@
 AddIs  [vimageI];
 AddSEs [vimageE];
 
-val ZF_cs = !claset;
-
-val eq_cs = ZF_cs addSIs [equalityI];
+val ZF_cs = !claset delrules [equalityI];
 
 (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
 goal thy "!!S. (ALL x:S. EX A B. x <= A*B) ==>  \
@@ -208,10 +206,10 @@
 
 
 goal thy "!!r. [| <a,c> : r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)";
-by (deepen_tac eq_cs 0 1);
+by (Deepen_tac 0 1);
 qed "domain_Diff_eq";
 
 goal thy "!!r. [| <c,b> : r; c~=a |] ==> range(r-{<a,b>}) = range(r)";
-by (deepen_tac eq_cs 0 1);
+by (Deepen_tac 0 1);
 qed "range_Diff_eq";
 
diff -r 88f15198950f -r bdeb5024353a src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/equalities.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -11,23 +11,23 @@
 
 (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
 goal thy "{a} Un B = cons(a,B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "cons_eq";
 
 goal thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "cons_commute";
 
 goal thy "!!B. a: B ==> cons(a,B) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "cons_absorb";
 
 goal thy "!!B. a: B ==> cons(a, B-{a}) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "cons_Diff";
 
 goal thy "!!C. [| a: C;  ALL y:C. y=b |] ==> C = {b}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "equal_singleton_lemma";
 val equal_singleton = ballI RSN (2,equal_singleton_lemma);
 
@@ -36,101 +36,101 @@
 
 (*NOT an equality, but it seems to belong here...*)
 goal thy "cons(a,B) Int C <= cons(a, B Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_cons";
 
 goal thy "A Int A = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_absorb";
 
 goal thy "A Int B = B Int A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_commute";
 
 goal thy "(A Int B) Int C  =  A Int (B Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_assoc";
 
 goal thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_Un_distrib";
 
 goal thy "A<=B <-> A Int B = A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Int_iff";
 
 goal thy "A<=B <-> B Int A = A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Int_iff2";
 
 goal thy "!!A B C. C<=A ==> (A-B) Int C = C-B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_Diff_eq";
 
 (** Binary Union **)
 
 goal thy "cons(a,B) Un C = cons(a, B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_cons";
 
 goal thy "A Un A = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_absorb";
 
 goal thy "A Un B = B Un A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_commute";
 
 goal thy "(A Un B) Un C  =  A Un (B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_assoc";
 
 goal thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_Int_distrib";
 
 goal thy "A<=B <-> A Un B = B";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Un_iff";
 
 goal thy "A<=B <-> B Un A = B";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_Un_iff2";
 
 (** Simple properties of Diff -- set difference **)
 
 goal thy "A-A = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_cancel";
 
 goal thy "0-A = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "empty_Diff";
 
 goal thy "A-0 = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_0";
 
 goal thy "A-B=0 <-> A<=B";
-by (fast_tac (eq_cs addEs [equalityE]) 1);
+by (fast_tac (!claset addEs [equalityE]) 1);
 qed "Diff_eq_0_iff";
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
 goal thy "A - cons(a,B) = A - B - {a}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_cons";
 
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
 goal thy "A - cons(a,B) = A - {a} - B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_cons2";
 
 goal thy "A Int (B-A) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_disjoint";
 
 goal thy "!!A B. A<=B ==> A Un (B-A) = B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_partition";
 
 goal thy "A <= B Un (A - B)";
@@ -138,40 +138,40 @@
 qed "subset_Un_Diff";
 
 goal thy "!!A B. [| A<=B; B<=C |] ==> B-(C-A) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "double_complement";
 
 goal thy "(A Un B) - (B-A) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "double_complement_Un";
 
 goal thy
  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_Int_crazy";
 
 goal thy "A - (B Un C) = (A-B) Int (A-C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_Un";
 
 goal thy "A - (B Int C) = (A-B) Un (A-C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_Int";
 
 (*Halmos, Naive Set Theory, page 16.*)
 goal thy "(A Int B) Un C = A Int (B Un C)  <->  C<=A";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "Un_Int_assoc_iff";
 
 
 (** Big Union and Intersection **)
 
 goal thy "Union(cons(a,B)) = a Un Union(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Union_cons";
 
 goal thy "Union(A Un B) = Union(A) Un Union(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Union_Un_distrib";
 
 goal thy "Union(A Int B) <= Union(A) Int Union(B)";
@@ -179,11 +179,11 @@
 qed "Union_Int_subset";
 
 goal thy "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
 goalw thy [Inter_def] "Inter(0) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Inter_0";
 
 goal thy "!!A B. [| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
@@ -192,70 +192,70 @@
 
 (* A good challenge: Inter is ill-behaved on the empty set *)
 goal thy "!!A B. [| a:A;  b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Inter_Un_distrib";
 
 goal thy "Union({b}) = b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Union_singleton";
 
 goal thy "Inter({b}) = b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Inter_singleton";
 
 (** Unions and Intersections of Families **)
 
 goal thy "Union(A) = (UN x:A. x)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Union_eq_UN";
 
 goalw thy [Inter_def] "Inter(A) = (INT x:A. x)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Inter_eq_INT";
 
 goal thy "(UN i:0. A(i)) = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "UN_0";
 
 (*Halmos, Naive Set Theory, page 35.*)
 goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_UN_distrib";
 
 goal thy "!!A B. i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_INT_distrib";
 
 goal thy
     "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_UN_distrib2";
 
 goal thy
     "!!I J. [| i:I;  j:J |] ==> \
 \    (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Un_INT_distrib2";
 
 goal thy "!!A. a: A ==> (UN y:A. c) = c";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "UN_constant";
 
 goal thy "!!A. a: A ==> (INT y:A. c) = c";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "INT_constant";
 
 (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
     Union of a family of unions **)
 
 goal thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "UN_Un_distrib";
 
 goal thy
     "!!A B. i:I ==> \
 \           (INT i:I. A(i)  Int  B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "INT_Int_distrib";
 
 goal thy "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))";
@@ -265,47 +265,47 @@
 (** Devlin, page 12, exercise 5: Complements **)
 
 goal thy "!!A B. i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_UN";
 
 goal thy "!!A B. i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Diff_INT";
 
 (** Unions and Intersections with General Sum **)
 
 (*Not suitable for rewriting: LOOPS!*)
 goal thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Sigma_cons1";
 
 (*Not suitable for rewriting: LOOPS!*)
 goal thy "A * cons(b,B) = A*{b} Un A*B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Sigma_cons2";
 
 goal thy "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Sigma_succ1";
 
 goal thy "A * succ(B) = A*{B} Un A*B";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Sigma_succ2";
 
 goal thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "SUM_UN_distrib1";
 
 goal thy "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "SUM_UN_distrib2";
 
 goal thy "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "SUM_Un_distrib1";
 
 goal thy "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "SUM_Un_distrib2";
 
 (*First-order version of the above, for rewriting*)
@@ -314,12 +314,12 @@
 qed "prod_Un_distrib2";
 
 goal thy "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "SUM_Int_distrib1";
 
 goal thy
     "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "SUM_Int_distrib2";
 
 (*First-order version of the above, for rewriting*)
@@ -329,35 +329,35 @@
 
 (*Cf Aczel, Non-Well-Founded Sets, page 115*)
 goal thy "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "SUM_eq_UN";
 
 (** Domain **)
 
 qed_goal "domain_of_prod" thy "!!A B. b:B ==> domain(A*B) = A"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
 
 qed_goal "domain_0" thy "domain(0) = 0"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
 
 qed_goal "domain_cons" thy
     "domain(cons(<a,b>,r)) = cons(a, domain(r))"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
 
 goal thy "domain(A Un B) = domain(A) Un domain(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_Un_eq";
 
 goal thy "domain(A Int B) <= domain(A) Int domain(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_Int_subset";
 
 goal thy "domain(A) - domain(B) <= domain(A - B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_Diff_subset";
 
 goal thy "domain(converse(r)) = range(r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_converse";
 
 Addsimps [domain_0, domain_cons, domain_Un_eq, domain_converse];
@@ -367,17 +367,17 @@
 
 qed_goal "range_of_prod" thy
     "!!a A B. a:A ==> range(A*B) = B"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
 
 qed_goal "range_0" thy "range(0) = 0"
- (fn _ => [ fast_tac eq_cs 1 ]); 
+ (fn _ => [ Fast_tac 1 ]); 
 
 qed_goal "range_cons" thy
     "range(cons(<a,b>,r)) = cons(b, range(r))"
- (fn _ => [ fast_tac eq_cs 1 ]);
+ (fn _ => [ Fast_tac 1 ]);
 
 goal thy "range(A Un B) = range(A) Un range(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "range_Un_eq";
 
 goal thy "range(A Int B) <= range(A) Int range(B)";
@@ -385,11 +385,11 @@
 qed "range_Int_subset";
 
 goal thy "range(A) - range(B) <= range(A - B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "range_Diff_subset";
 
 goal thy "range(converse(r)) = domain(r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "range_converse";
 
 Addsimps [range_0, range_cons, range_Un_eq, range_converse];
@@ -398,29 +398,29 @@
 (** Field **)
 
 qed_goal "field_of_prod" thy "field(A*A) = A"
- (fn _ => [ fast_tac eq_cs 1 ]); 
+ (fn _ => [ Fast_tac 1 ]); 
 
 qed_goal "field_0" thy "field(0) = 0"
- (fn _ => [ fast_tac eq_cs 1 ]); 
+ (fn _ => [ Fast_tac 1 ]); 
 
 qed_goal "field_cons" thy
     "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
  (fn _ => [ rtac equalityI 1, ALLGOALS (Fast_tac) ]);
 
 goal thy "field(A Un B) = field(A) Un field(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "field_Un_eq";
 
 goal thy "field(A Int B) <= field(A) Int field(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "field_Int_subset";
 
 goal thy "field(A) - field(B) <= field(A - B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "field_Diff_subset";
 
 goal thy "field(converse(r)) = field(r)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "field_converse";
 
 Addsimps [field_0, field_cons, field_Un_eq, field_converse];
@@ -429,11 +429,11 @@
 (** Image **)
 
 goal thy "r``0 = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "image_0";
 
 goal thy "r``(A Un B) = (r``A) Un (r``B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "image_Un";
 
 goal thy "r``(A Int B) <= (r``A) Int (r``B)";
@@ -445,7 +445,7 @@
 qed "image_Int_square_subset";
 
 goal thy "!!r. B<=A ==> (r Int A*A)``B = (r``B) Int A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "image_Int_square";
 
 Addsimps [image_0, image_Un];
@@ -454,11 +454,11 @@
 (** Inverse Image **)
 
 goal thy "r-``0 = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "vimage_0";
 
 goal thy "r-``(A Un B) = (r-``A) Un (r-``B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "vimage_Un";
 
 goal thy "r-``(A Int B) <= (r-``A) Int (r-``B)";
@@ -470,7 +470,7 @@
 qed "vimage_Int_square_subset";
 
 goal thy "!!r. B<=A ==> (r Int A*A)-``B = (r-``B) Int A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "vimage_Int_square";
 
 Addsimps [vimage_0, vimage_Un];
@@ -479,24 +479,24 @@
 (** Converse **)
 
 goal thy "converse(A Un B) = converse(A) Un converse(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "converse_Un";
 
 goal thy "converse(A Int B) = converse(A) Int converse(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "converse_Int";
 
 goal thy "converse(A - B) = converse(A) - converse(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "converse_Diff";
 
 goal thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "converse_UN";
 
 (*Unfolding Inter avoids using excluded middle on A=0*)
 goalw thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "converse_INT";
 
 Addsimps [converse_Un, converse_Int, converse_Diff, converse_UN, converse_INT];
@@ -516,15 +516,15 @@
 qed "subset_Pow_Union";
 
 goal thy "Union(Pow(A)) = A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Union_Pow_eq";
 
 goal thy "Pow(A Int B) = Pow(A) Int Pow(B)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Int_Pow_eq";
 
 goal thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "INT_Pow_subset";
 
 Addsimps [Union_Pow_eq, Int_Pow_eq];
@@ -532,25 +532,25 @@
 (** RepFun **)
 
 goal thy "{f(x).x:A}=0 <-> A=0";
-by (fast_tac (eq_cs addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "RepFun_eq_0_iff";
 
 (** Collect **)
 
 goal thy "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Collect_Un";
 
 goal thy "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Collect_Int";
 
 goal thy "Collect(A - B, P) = Collect(A,P) - Collect(B,P)";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Collect_Diff";
 
 goal thy "{x:cons(a,B). P(x)} = if(P(a), cons(a, {x:B. P(x)}), {x:B. P(x)})";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Collect_cons";
 
diff -r 88f15198950f -r bdeb5024353a src/ZF/ex/Brouwer.ML
--- a/src/ZF/ex/Brouwer.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Brouwer.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -14,7 +14,7 @@
 
 goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
 let open brouwer;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "brouwer_unfold";
@@ -38,7 +38,7 @@
 
 goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
 let open Well;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "Well_unfold";
diff -r 88f15198950f -r bdeb5024353a src/ZF/ex/Data.ML
--- a/src/ZF/ex/Data.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Data.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -11,7 +11,7 @@
 
 goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
 let open data;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "data_unfold";
diff -r 88f15198950f -r bdeb5024353a src/ZF/ex/Mutil.ML
--- a/src/ZF/ex/Mutil.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Mutil.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -12,7 +12,7 @@
 (** Basic properties of evnodd **)
 
 goalw thy [evnodd_def] "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "evnodd_iff";
 
 goalw thy [evnodd_def] "evnodd(A, b) <= A";
@@ -103,16 +103,16 @@
 by (assume_tac 2);
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
     "{i}*{succ(n1#+n1)} Un {i}*{n1#+n1} = {<i,n1#+n1>, <i,succ(n1#+n1)>}" 1);
-by (fast_tac eq_cs 2);
+by (Fast_tac 2);
 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (fast_tac (eq_cs addEs [mem_irrefl, mem_asym]) 1);
+by (fast_tac (!claset addEs [mem_irrefl, mem_asym]) 1);
 qed "dominoes_tile_row";
 
 goal thy "!!m n. [| m: nat;  n: nat |] ==> m * (n #+ n) : tiling(domino)";
 by (nat_ind_tac "m" [] 1);
 by (simp_tac (!simpset addsimps tiling.intrs) 1);
 by (asm_simp_tac (!simpset addsimps [Sigma_succ1]) 1);
-by (fast_tac (eq_cs addIs [tiling_UnI, dominoes_tile_row] 
+by (fast_tac (!claset addIs [tiling_UnI, dominoes_tile_row] 
                     addEs [mem_irrefl]) 1);
 qed "dominoes_tile_matrix";
 
diff -r 88f15198950f -r bdeb5024353a src/ZF/ex/Ntree.ML
--- a/src/ZF/ex/Ntree.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Ntree.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -15,7 +15,7 @@
 
 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
 let open ntree;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "ntree_unfold";
@@ -70,7 +70,7 @@
 
 goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
 let open maptree;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "maptree_unfold";
@@ -95,7 +95,7 @@
 
 goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
 let open maptree2;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "maptree2_unfold";
diff -r 88f15198950f -r bdeb5024353a src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/TF.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -38,7 +38,7 @@
     "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
 let open tree_forest;  
     val rew = rewrite_rule (con_defs @ tl defs) in  
-by (fast_tac (sum_cs addSIs (equalityI :: (map rew intrs RL [PartD1]))
+by (fast_tac (!claset addSIs (equalityI :: (map rew intrs RL [PartD1]))
                      addEs [rew elim]) 1)
 end;
 qed "tree_forest_unfold";
diff -r 88f15198950f -r bdeb5024353a src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Term.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -11,7 +11,7 @@
 
 goal Term.thy "term(A) = A * list(term(A))";
 let open term;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "term_unfold";
diff -r 88f15198950f -r bdeb5024353a src/ZF/func.ML
--- a/src/ZF/func.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/func.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -53,11 +53,11 @@
 
 (*Empty function spaces*)
 goalw thy [Pi_def, function_def] "Pi(0,A) = {0}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Pi_empty1";
 
 goalw thy [Pi_def] "!!A a. a:A ==> A->0 = 0";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "Pi_empty2";
 
 (*The empty function*)
@@ -67,7 +67,7 @@
 
 (*The singleton function*)
 goalw thy [Pi_def, function_def] "{<a,b>} : {a} -> {b}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "singleton_fun";
 
 Addsimps [empty_fun, singleton_fun];
@@ -245,7 +245,7 @@
 (** Images of functions **)
 
 goalw thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "image_lam";
 
 goal thy "!!C A. [| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}";
@@ -291,7 +291,7 @@
 qed "restrict_eqI";
 
 goalw thy [restrict_def, lam_def] "domain(restrict(f,C)) = C";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_restrict";
 
 val [prem] = goalw thy [restrict_def]
@@ -360,7 +360,7 @@
 (** Domain and range of a function/relation **)
 
 goalw thy [Pi_def] "!!f. f : Pi(A,B) ==> domain(f)=A";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "domain_of_fun";
 
 goal thy "!!f. [| f : Pi(A,B);  a: A |] ==> f`a : range(f)";
@@ -379,7 +379,7 @@
     "!!f A B. [| f: A->B;  c~:A |] ==> cons(<c,b>,f) : cons(c,A) -> cons(b,B)";
 by (forward_tac [singleton_fun RS fun_disjoint_Un] 1);
 by (asm_full_simp_tac (FOL_ss addsimps [cons_eq]) 2);
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "fun_extend";
 
 goal thy
@@ -417,6 +417,6 @@
 by (etac consE 1);
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [restrict, fun_extend_apply1, 
-				      fun_extend_apply2])));
+                                      fun_extend_apply2])));
 qed "cons_fun_eq";
 
diff -r 88f15198950f -r bdeb5024353a src/ZF/pair.ML
--- a/src/ZF/pair.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/pair.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -99,10 +99,10 @@
 AddSEs [SigmaE2, SigmaE];
 
 qed_goal "Sigma_empty1" thy "Sigma(0,B) = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 qed_goal "Sigma_empty2" thy "A*0 = 0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _ => [ (Fast_tac 1) ]);
 
 Addsimps [Sigma_empty1, Sigma_empty2];
 
diff -r 88f15198950f -r bdeb5024353a src/ZF/subset.ML
--- a/src/ZF/subset.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/subset.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -23,7 +23,7 @@
 bind_thm ("cons_subsetE", cons_subset_iff RS iffD1 RS conjE);
 
 qed_goal "subset_empty_iff" thy "A<=0 <-> A=0"
- (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
+ (fn _=> [ (Fast_tac 1) ]);
 
 qed_goal "subset_cons_iff" thy
     "C<=cons(a,B) <-> C<=B | (a:C & C-{a} <= B)"
@@ -73,7 +73,7 @@
 (*** Union of a family of sets  ***)
 
 goal thy "A <= (UN i:I. B(i)) <-> A = (UN i:I. A Int B(i))";
-by (fast_tac (!claset addSIs [equalityI] addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE]) 1);
 qed "subset_UN_iff_eq";
 
 qed_goal "UN_subset_iff" thy
diff -r 88f15198950f -r bdeb5024353a src/ZF/upair.ML
--- a/src/ZF/upair.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/upair.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -198,8 +198,7 @@
 qed_goalw "the_equality" thy [the_def]
     "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
  (fn [pa,eq] =>
-  [ (fast_tac (!claset addSIs [pa] addIs [equalityI]
-	               addEs [eq RS subst]) 1) ]);
+  [ (fast_tac (!claset addSIs [pa] addEs [eq RS subst]) 1) ]);
 
 (* Only use this if you already know EX!x. P(x) *)
 qed_goal "the_equality2" thy
@@ -226,7 +225,7 @@
 (*If it's "undefined", it's zero!*)
 qed_goalw "the_0" thy [the_def]
     "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
- (fn _ => [ (fast_tac (!claset addIs [equalityI] addSEs [ReplaceE]) 1) ]);
+ (fn _ => [ (fast_tac (!claset addSEs [ReplaceE]) 1) ]);
 
 
 (*** if -- a conditional expression for formulae ***)