src/HOL/RelPow.ML
changeset 1760 6f41a494f3b1
parent 1693 7083f6b05423
child 2031 03a843f0f447
     1.1 --- a/src/HOL/RelPow.ML	Wed May 22 18:32:37 1996 +0200
     1.2 +++ b/src/HOL/RelPow.ML	Thu May 23 14:37:06 1996 +0200
     1.3 @@ -20,15 +20,15 @@
     1.4  
     1.5  goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
     1.6  by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
     1.7 -by (fast_tac comp_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "rel_pow_Suc_I";
    1.10  
    1.11  goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    1.12  by (nat_ind_tac "n" 1);
    1.13  by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.14 -by (fast_tac comp_cs 1);
    1.15 +by (Fast_tac 1);
    1.16  by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.17 -by (fast_tac comp_cs 1);
    1.18 +by (Fast_tac 1);
    1.19  qed_spec_mp "rel_pow_Suc_I2";
    1.20  
    1.21  goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
    1.22 @@ -39,7 +39,7 @@
    1.23    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
    1.24  by (cut_facts_tac [major] 1);
    1.25  by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    1.26 -by (fast_tac (comp_cs addIs [minor]) 1);
    1.27 +by (fast_tac (!claset addIs [minor]) 1);
    1.28  qed "rel_pow_Suc_E";
    1.29  
    1.30  val [p1,p2,p3] = goal RelPow.thy
    1.31 @@ -57,8 +57,8 @@
    1.32  
    1.33  goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
    1.34  by (nat_ind_tac "n" 1);
    1.35 -by (fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    1.36 -by (fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    1.37 +by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    1.38 +by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    1.39  qed_spec_mp "rel_pow_Suc_D2";
    1.40  
    1.41  val [p1,p2,p3] = goal RelPow.thy
    1.42 @@ -80,13 +80,13 @@
    1.43  goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
    1.44  by (split_all_tac 1);
    1.45  by (etac rtrancl_induct 1);
    1.46 -by (ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
    1.47 +by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
    1.48  qed "rtrancl_imp_UN_rel_pow";
    1.49  
    1.50  goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
    1.51  by (nat_ind_tac "n" 1);
    1.52 -by (fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
    1.53 -by (fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
    1.54 +by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
    1.55 +by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
    1.56  val lemma = result() RS spec RS mp;
    1.57  
    1.58  goal RelPow.thy "!!p. p:R^n ==> p:R^*";
    1.59 @@ -95,5 +95,5 @@
    1.60  qed "rel_pow_imp_rtrancl";
    1.61  
    1.62  goal RelPow.thy "R^* = (UN n. R^n)";
    1.63 -by (fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
    1.64 +by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
    1.65  qed "rtrancl_is_UN_rel_pow";