src/HOL/RelPow.ML

--- a/src/HOL/RelPow.ML	Wed May 22 18:32:37 1996 +0200
+++ b/src/HOL/RelPow.ML	Thu May 23 14:37:06 1996 +0200
@@ -20,15 +20,15 @@
 
 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed "rel_pow_Suc_I";
 
 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
 by (nat_ind_tac "n" 1);
 by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac comp_cs 1);
+by (Fast_tac 1);
 qed_spec_mp "rel_pow_Suc_I2";
 
 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
@@ -39,7 +39,7 @@
   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
 by (cut_facts_tac [major] 1);
 by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by (fast_tac (comp_cs addIs [minor]) 1);
+by (fast_tac (!claset addIs [minor]) 1);
 qed "rel_pow_Suc_E";
 
 val [p1,p2,p3] = goal RelPow.thy
@@ -57,8 +57,8 @@
 
 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
 by (nat_ind_tac "n" 1);
-by (fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by (fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
 qed_spec_mp "rel_pow_Suc_D2";
 
 val [p1,p2,p3] = goal RelPow.thy
@@ -80,13 +80,13 @@
 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
 by (split_all_tac 1);
 by (etac rtrancl_induct 1);
-by (ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
+by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
 qed "rtrancl_imp_UN_rel_pow";
 
 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
 by (nat_ind_tac "n" 1);
-by (fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
-by (fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
+by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
+by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
 val lemma = result() RS spec RS mp;
 
 goal RelPow.thy "!!p. p:R^n ==> p:R^*";
@@ -95,5 +95,5 @@
 qed "rel_pow_imp_rtrancl";
 
 goal RelPow.thy "R^* = (UN n. R^n)";
-by (fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
+by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";