src/HOL/Finite.ML
changeset 1760 6f41a494f3b1
parent 1660 8cb42cd97579
child 1782 ab45b881fa62
     1.1 --- a/src/HOL/Finite.ML	Wed May 22 18:32:37 1996 +0200
     1.2 +++ b/src/HOL/Finite.ML	Thu May 23 14:37:06 1996 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  qed "Fin_mono";
     1.5  
     1.6  goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
     1.7 -by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
     1.8 +by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
     1.9  qed "Fin_subset_Pow";
    1.10  
    1.11  (* A : Fin(B) ==> A <= B *)
    1.12 @@ -55,7 +55,7 @@
    1.13  qed "Fin_subset";
    1.14  
    1.15  goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
    1.16 -by (fast_tac (set_cs addIs [Fin_UnI] addDs
    1.17 +by (fast_tac (!claset addIs [Fin_UnI] addDs
    1.18                  [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
    1.19  qed "subset_Fin";
    1.20  Addsimps[subset_Fin];
    1.21 @@ -63,7 +63,7 @@
    1.22  goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
    1.23  by (stac insert_is_Un 1);
    1.24  by (Simp_tac 1);
    1.25 -by (fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
    1.26 +by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
    1.27  qed "insert_Fin";
    1.28  Addsimps[insert_Fin];
    1.29  
    1.30 @@ -163,7 +163,7 @@
    1.31  section "Finite cardinality -- 'card'";
    1.32  
    1.33  goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
    1.34 -by (fast_tac eq_cs 1);
    1.35 +by (Fast_tac 1);
    1.36  val Collect_conv_insert = result();
    1.37  
    1.38  goalw Finite.thy [card_def] "card {} = 0";
    1.39 @@ -197,7 +197,7 @@
    1.40  by (case_tac "? a. a:A" 1);
    1.41   by (res_inst_tac [("x","0")] exI 2);
    1.42   by (Simp_tac 2);
    1.43 - by (fast_tac eq_cs 2);
    1.44 + by (Fast_tac 2);
    1.45  by (etac exE 1);
    1.46  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    1.47  by (rtac exI 1);
    1.48 @@ -212,7 +212,7 @@
    1.49    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    1.50    by (SELECT_GOAL(safe_tac eq_cs)1);
    1.51     by (subgoal_tac "x ~= f m" 1);
    1.52 -    by (fast_tac set_cs 2);
    1.53 +    by (Fast_tac 2);
    1.54     by (subgoal_tac "? k. f k = x & k<m" 1);
    1.55      by (best_tac set_cs 2);
    1.56     by (SELECT_GOAL(safe_tac HOL_cs)1);
    1.57 @@ -226,7 +226,7 @@
    1.58   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    1.59   by (SELECT_GOAL(safe_tac eq_cs)1);
    1.60    by (subgoal_tac "x ~= f m" 1);
    1.61 -   by (fast_tac set_cs 2);
    1.62 +   by (Fast_tac 2);
    1.63    by (subgoal_tac "? k. f k = x & k<m" 1);
    1.64     by (best_tac set_cs 2);
    1.65    by (SELECT_GOAL(safe_tac HOL_cs)1);
    1.66 @@ -237,7 +237,7 @@
    1.67  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
    1.68  by (SELECT_GOAL(safe_tac eq_cs)1);
    1.69   by (subgoal_tac "x ~= f i" 1);
    1.70 -  by (fast_tac set_cs 2);
    1.71 +  by (Fast_tac 2);
    1.72   by (case_tac "x = f m" 1);
    1.73    by (res_inst_tac [("x","i")] exI 1);
    1.74    by (Asm_simp_tac 1);
    1.75 @@ -305,8 +305,8 @@
    1.76  by (Asm_simp_tac 1);
    1.77  by (rtac card_insert_disjoint 1);
    1.78  by (rtac (major RSN (2,finite_subset)) 1);
    1.79 -by (fast_tac set_cs 1);
    1.80 -by (fast_tac HOL_cs 1);
    1.81 +by (Fast_tac 1);
    1.82 +by (Fast_tac 1);
    1.83  by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
    1.84  qed "card_insert";
    1.85  Addsimps [card_insert];