src/HOL/Finite.ML
changeset 1786 8a31d85d27b8
parent 1782 ab45b881fa62
child 2031 03a843f0f447
     1.1 --- a/src/HOL/Finite.ML	Mon Jun 03 11:44:44 1996 +0200
     1.2 +++ b/src/HOL/Finite.ML	Mon Jun 03 17:10:56 1996 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4              rtac subs]);
     1.5  by (rtac (fin RS Fin_induct) 1);
     1.6  by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
     1.7 -by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
     1.8 +by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
     1.9  by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    1.10  by (ALLGOALS Asm_simp_tac);
    1.11  qed "Fin_subset";
    1.12 @@ -205,47 +205,47 @@
    1.13  by (etac equalityE 1);
    1.14  by (asm_full_simp_tac
    1.15       (!simpset addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
    1.16 -by (SELECT_GOAL(safe_tac eq_cs)1);
    1.17 +by (SELECT_GOAL(safe_tac (!claset))1);
    1.18    by (Asm_full_simp_tac 1);
    1.19    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    1.20 -  by (SELECT_GOAL(safe_tac eq_cs)1);
    1.21 +  by (SELECT_GOAL(safe_tac (!claset))1);
    1.22     by (subgoal_tac "x ~= f m" 1);
    1.23      by (Fast_tac 2);
    1.24     by (subgoal_tac "? k. f k = x & k<m" 1);
    1.25 -    by (best_tac set_cs 2);
    1.26 -   by (SELECT_GOAL(safe_tac HOL_cs)1);
    1.27 +    by (best_tac (!claset) 2);
    1.28 +   by (SELECT_GOAL(safe_tac (!claset))1);
    1.29     by (res_inst_tac [("x","k")] exI 1);
    1.30     by (Asm_simp_tac 1);
    1.31    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    1.32 -  by (best_tac set_cs 1);
    1.33 +  by (best_tac (!claset) 1);
    1.34   bd sym 1;
    1.35   by (rotate_tac ~1 1);
    1.36   by (Asm_full_simp_tac 1);
    1.37   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    1.38 - by (SELECT_GOAL(safe_tac eq_cs)1);
    1.39 + by (SELECT_GOAL(safe_tac (!claset))1);
    1.40    by (subgoal_tac "x ~= f m" 1);
    1.41     by (Fast_tac 2);
    1.42    by (subgoal_tac "? k. f k = x & k<m" 1);
    1.43 -   by (best_tac set_cs 2);
    1.44 -  by (SELECT_GOAL(safe_tac HOL_cs)1);
    1.45 +   by (best_tac (!claset) 2);
    1.46 +  by (SELECT_GOAL(safe_tac (!claset))1);
    1.47    by (res_inst_tac [("x","k")] exI 1);
    1.48    by (Asm_simp_tac 1);
    1.49   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    1.50 - by (best_tac set_cs 1);
    1.51 + by (best_tac (!claset) 1);
    1.52  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
    1.53 -by (SELECT_GOAL(safe_tac eq_cs)1);
    1.54 +by (SELECT_GOAL(safe_tac (!claset))1);
    1.55   by (subgoal_tac "x ~= f i" 1);
    1.56    by (Fast_tac 2);
    1.57   by (case_tac "x = f m" 1);
    1.58    by (res_inst_tac [("x","i")] exI 1);
    1.59    by (Asm_simp_tac 1);
    1.60   by (subgoal_tac "? k. f k = x & k<m" 1);
    1.61 -  by (best_tac set_cs 2);
    1.62 - by (SELECT_GOAL(safe_tac HOL_cs)1);
    1.63 +  by (best_tac (!claset) 2);
    1.64 + by (SELECT_GOAL(safe_tac (!claset))1);
    1.65   by (res_inst_tac [("x","k")] exI 1);
    1.66   by (Asm_simp_tac 1);
    1.67  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    1.68 -by (best_tac set_cs 1);
    1.69 +by (best_tac (!claset) 1);
    1.70  val lemma = result();
    1.71  
    1.72  goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
    1.73 @@ -316,7 +316,7 @@
    1.74  by (strip_tac 1);
    1.75  by (case_tac "x:B" 1);
    1.76   by (dtac mk_disjoint_insert 1);
    1.77 - by (SELECT_GOAL(safe_tac HOL_cs)1);
    1.78 + by (SELECT_GOAL(safe_tac (!claset))1);
    1.79   by (rotate_tac ~1 1);
    1.80   by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
    1.81  by (rotate_tac ~1 1);