src/HOL/Arith.ML
changeset 3919 c036caebfc75
parent 3903 1b29151a1009
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/Arith.ML	Fri Oct 17 15:23:14 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Oct 17 15:25:12 1997 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  AddIffs [pred_le];
     1.5  
     1.6  goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
     1.7 -by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
     1.8 +by(simp_tac (!simpset addsplits [expand_nat_case]) 1);
     1.9  qed_spec_mp "pred_le_mono";
    1.10  
    1.11  goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
    1.12 @@ -434,7 +434,7 @@
    1.13  
    1.14  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.15  by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
    1.16 -                    setloop (split_tac [expand_if])) 1);
    1.17 +                       addsplits [expand_if]) 1);
    1.18  qed "if_Suc_diff_n";
    1.19  
    1.20  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";