src/HOL/arith_data.ML
changeset 5418 a895ab904b85
parent 5353 0526ade4a23b
child 5429 0833486c23ce
     1.1 --- a/src/HOL/arith_data.ML	Tue Sep 01 15:04:59 1998 +0200
     1.2 +++ b/src/HOL/arith_data.ML	Tue Sep 01 15:05:36 1998 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4  by (Clarify_tac 1);
     1.5  by (etac less_SucE 1);
     1.6  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
     1.7 -				      Suc_diff_n]) 1);
     1.8 +				      Suc_diff_le]) 1);
     1.9  by (Clarify_tac 1);
    1.10  by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    1.11  qed_spec_mp "diff_less_mono2";