src/HOL/Arith.ML
changeset 4686 74a12e86b20b
parent 4672 9d55bc687e1e
child 4732 10af4886b33f
     1.1 --- a/src/HOL/Arith.ML	Fri Mar 06 18:25:28 1998 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sat Mar 07 16:29:29 1998 +0100
     1.3 @@ -433,12 +433,11 @@
     1.4  qed "less_imp_diff_positive";
     1.5  
     1.6  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
     1.7 -by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
     1.8 -                       addsplits [expand_if]) 1);
     1.9 +by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]) 1);
    1.10  qed "if_Suc_diff_n";
    1.11  
    1.12  goal Arith.thy "Suc(m)-n <= Suc(m-n)";
    1.13 -by (simp_tac (simpset() addsimps [if_Suc_diff_n] addsplits [expand_if]) 1);
    1.14 +by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
    1.15  qed "diff_Suc_le_Suc_diff";
    1.16  
    1.17  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";