src/HOL/Finite.ML

 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
 qed "Fin_mono";
 
 goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
-by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
+by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
 qed "Fin_subset_Pow";
 
 (* A : Fin(B) ==> A <= B *)
 val FinD = Fin_subset_Pow RS subsetD RS PowD;
 

 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
 by (ALLGOALS Asm_simp_tac);
 qed "Fin_subset";
 
 goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
-by (fast_tac (set_cs addIs [Fin_UnI] addDs
+by (fast_tac (!claset addIs [Fin_UnI] addDs
                 [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
 qed "subset_Fin";
 Addsimps[subset_Fin];
 
 goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
 by (stac insert_is_Un 1);
 by (Simp_tac 1);
-by (fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
+by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
 qed "insert_Fin";
 Addsimps[insert_Fin];
 
 (*The image of a finite set is finite*)
 val major::_ = goal Finite.thy

 
 
 section "Finite cardinality -- 'card'";
 
 goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 val Collect_conv_insert = result();
 
 goalw Finite.thy [card_def] "card {} = 0";
 by (rtac Least_equality 1);
 by (ALLGOALS Asm_full_simp_tac);

 by (rename_tac "m" 1);
 by (hyp_subst_tac 1);
 by (case_tac "? a. a:A" 1);
  by (res_inst_tac [("x","0")] exI 2);
  by (Simp_tac 2);
- by (fast_tac eq_cs 2);
+ by (Fast_tac 2);
 by (etac exE 1);
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (rtac exI 1);
 by (rtac conjI 1);
  br disjI2 1;

 by (SELECT_GOAL(safe_tac eq_cs)1);
   by (Asm_full_simp_tac 1);
   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   by (SELECT_GOAL(safe_tac eq_cs)1);
    by (subgoal_tac "x ~= f m" 1);
-    by (fast_tac set_cs 2);
+    by (Fast_tac 2);
    by (subgoal_tac "? k. f k = x & k<m" 1);
     by (best_tac set_cs 2);
    by (SELECT_GOAL(safe_tac HOL_cs)1);
    by (res_inst_tac [("x","k")] exI 1);
    by (Asm_simp_tac 1);

  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
  by (SELECT_GOAL(safe_tac eq_cs)1);
   by (subgoal_tac "x ~= f m" 1);
-   by (fast_tac set_cs 2);
+   by (Fast_tac 2);
   by (subgoal_tac "? k. f k = x & k<m" 1);
    by (best_tac set_cs 2);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
   by (res_inst_tac [("x","k")] exI 1);
   by (Asm_simp_tac 1);
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  by (best_tac set_cs 1);
 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
 by (SELECT_GOAL(safe_tac eq_cs)1);
  by (subgoal_tac "x ~= f i" 1);
-  by (fast_tac set_cs 2);
+  by (Fast_tac 2);
  by (case_tac "x = f m" 1);
   by (res_inst_tac [("x","i")] exI 1);
   by (Asm_simp_tac 1);
  by (subgoal_tac "? k. f k = x & k<m" 1);
   by (best_tac set_cs 2);

 by (dtac mk_disjoint_insert 1);
 by (etac exE 1);
 by (Asm_simp_tac 1);
 by (rtac card_insert_disjoint 1);
 by (rtac (major RSN (2,finite_subset)) 1);
-by (fast_tac set_cs 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
+by (Fast_tac 1);
 by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
 qed "card_insert";
 Addsimps [card_insert];