src/HOL/Arith.ML
changeset 5183 89f162de39cf
parent 5143 b94cd208f073
child 5270 70c599bff977
     1.1 --- a/src/HOL/Arith.ML	Fri Jul 24 13:02:01 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Jul 24 13:03:20 1998 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4     However, none of the generalizations are currently in the simpset,
     1.5     and I dread to think what happens if I put them in *)
     1.6  Goal "0 < n ==> Suc(n-1) = n";
     1.7 -by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
     1.8 +by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
     1.9  qed "Suc_pred";
    1.10  Addsimps [Suc_pred];
    1.11  
    1.12 @@ -114,7 +114,7 @@
    1.13  Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.14  by (exhaust_tac "m" 1);
    1.15  by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
    1.16 -                                      addsplits [split_nat_case])));
    1.17 +                                      addsplits [nat.split])));
    1.18  qed "add_pred";
    1.19  Addsimps [add_pred];
    1.20  
    1.21 @@ -373,7 +373,7 @@
    1.22  Addsimps [Suc_diff_diff];
    1.23  
    1.24  Goal "0<n ==> n - Suc i < n";
    1.25 -by (res_inst_tac [("n","n")] natE 1);
    1.26 +by (exhaust_tac "n" 1);
    1.27  by Safe_tac;
    1.28  by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc RS sym]) 1);
    1.29  qed "diff_Suc_less";
    1.30 @@ -670,8 +670,8 @@
    1.31  Goal "!!n::nat. m<=n ==> (l-n) <= (l-m)";
    1.32  by (induct_tac "l" 1);
    1.33  by (Simp_tac 1);
    1.34 -by (case_tac "n <= l" 1);
    1.35 -by (subgoal_tac "m <= l" 1);
    1.36 +by (case_tac "n <= na" 1);
    1.37 +by (subgoal_tac "m <= na" 1);
    1.38  by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
    1.39  by (fast_tac (claset() addEs [le_trans]) 1);
    1.40  by (dtac not_leE 1);