# HG changeset patch
# User paulson
# Date 904655136 -7200
# Node ID a895ab904b85ca7d48715892b93519e3246ec987
# Parent  1f533238b53bea5eb65286815bc0d891ec7490f3
Replaced Suc_diff_n by Suc_diff_le

diff -r 1f533238b53b -r a895ab904b85 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Tue Sep 01 15:04:59 1998 +0200
+++ b/src/HOL/arith_data.ML	Tue Sep 01 15:05:36 1998 +0200
@@ -228,7 +228,7 @@
 by (Clarify_tac 1);
 by (etac less_SucE 1);
 by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
-				      Suc_diff_n]) 1);
+				      Suc_diff_le]) 1);
 by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
 qed_spec_mp "diff_less_mono2";