Replaced Suc_diff_n by Suc_diff_le
authorpaulson
Tue Sep 01 15:05:36 1998 +0200 (1998-09-01)
changeset 5418a895ab904b85
parent 5417 1f533238b53b
child 5419 3a744748dd21
Replaced Suc_diff_n by Suc_diff_le
src/HOL/arith_data.ML
     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";