src/HOL/Finite.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4304 af2a2cd9fa51
     1.1 --- a/src/HOL/Finite.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/Finite.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -154,8 +154,8 @@
     1.4  
     1.5  val [prem] = goal Finite.thy
     1.6   "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
     1.7 -br (prem RS finite_induct) 1;
     1.8 -by(ALLGOALS Asm_simp_tac);
     1.9 +by (rtac (prem RS finite_induct) 1);
    1.10 +by (ALLGOALS Asm_simp_tac);
    1.11  bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
    1.12  Addsimps [finite_UnionI];
    1.13  
    1.14 @@ -163,7 +163,7 @@
    1.15  
    1.16  goalw Finite.thy [Sigma_def]
    1.17   "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
    1.18 -by(blast_tac (claset() addSIs [finite_UnionI]) 1);
    1.19 +by (blast_tac (claset() addSIs [finite_UnionI]) 1);
    1.20  bind_thm("finite_SigmaI", ballI RSN (2,result()));
    1.21  Addsimps [finite_SigmaI];
    1.22  
    1.23 @@ -250,15 +250,15 @@
    1.24  by (etac equalityE 1);
    1.25  by (asm_full_simp_tac
    1.26       (simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
    1.27 -by (safe_tac (claset()));
    1.28 +by Safe_tac;
    1.29    by (Asm_full_simp_tac 1);
    1.30    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    1.31 -  by (SELECT_GOAL(safe_tac (claset()))1);
    1.32 +  by (SELECT_GOAL Safe_tac 1);
    1.33     by (subgoal_tac "x ~= f m" 1);
    1.34      by (Blast_tac 2);
    1.35     by (subgoal_tac "? k. f k = x & k<m" 1);
    1.36      by (Blast_tac 2);
    1.37 -   by (SELECT_GOAL(safe_tac (claset()))1);
    1.38 +   by (SELECT_GOAL Safe_tac 1);
    1.39     by (res_inst_tac [("x","k")] exI 1);
    1.40     by (Asm_simp_tac 1);
    1.41    by (simp_tac (simpset() addsplits [expand_if]) 1);
    1.42 @@ -267,18 +267,18 @@
    1.43   by (rotate_tac ~1 1);
    1.44   by (Asm_full_simp_tac 1);
    1.45   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    1.46 - by (SELECT_GOAL(safe_tac (claset()))1);
    1.47 + by (SELECT_GOAL Safe_tac 1);
    1.48    by (subgoal_tac "x ~= f m" 1);
    1.49     by (Blast_tac 2);
    1.50    by (subgoal_tac "? k. f k = x & k<m" 1);
    1.51     by (Blast_tac 2);
    1.52 -  by (SELECT_GOAL(safe_tac (claset()))1);
    1.53 +  by (SELECT_GOAL Safe_tac 1);
    1.54    by (res_inst_tac [("x","k")] exI 1);
    1.55    by (Asm_simp_tac 1);
    1.56   by (simp_tac (simpset() addsplits [expand_if]) 1);
    1.57   by (Blast_tac 1);
    1.58  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
    1.59 -by (SELECT_GOAL(safe_tac (claset()))1);
    1.60 +by (SELECT_GOAL Safe_tac 1);
    1.61   by (subgoal_tac "x ~= f i" 1);
    1.62    by (Blast_tac 2);
    1.63   by (case_tac "x = f m" 1);
    1.64 @@ -286,7 +286,7 @@
    1.65    by (Asm_simp_tac 1);
    1.66   by (subgoal_tac "? k. f k = x & k<m" 1);
    1.67    by (Blast_tac 2);
    1.68 - by (SELECT_GOAL(safe_tac (claset()))1);
    1.69 + by (SELECT_GOAL Safe_tac 1);
    1.70   by (res_inst_tac [("x","k")] exI 1);
    1.71   by (Asm_simp_tac 1);
    1.72  by (simp_tac (simpset() addsplits [expand_if]) 1);
    1.73 @@ -335,7 +335,7 @@
    1.74  by (Clarify_tac 1);
    1.75  by (case_tac "x:B" 1);
    1.76   by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
    1.77 - by (SELECT_GOAL(safe_tac (claset()))1);
    1.78 + by (SELECT_GOAL Safe_tac 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);