src/HOL/Arith.ML
changeset 4830 bd73675adbed
parent 4736 f7d3b9aec7a1
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Arith.ML	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Apr 27 16:45:11 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 thy "!!n. 0 < n ==> Suc(n-1) = n";
     1.7 -by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
     1.8 +by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
     1.9  qed "Suc_pred";
    1.10  Addsimps [Suc_pred];
    1.11  
    1.12 @@ -114,7 +114,7 @@
    1.13  goal thy "!!n. 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 [expand_nat_case])));
    1.17 +                                      addsplits [split_nat_case])));
    1.18  qed "add_pred";
    1.19  Addsimps [add_pred];
    1.20