# HG changeset patch
# User paulson
# Date 903624245 -7200
# Node ID 0526ade4a23b8078787f56a95e0c6691672dae6a
# Parent  a32312d17ed646087406ef6d3d622fd85e403514
adjusted for new rewrites

diff -r a32312d17ed6 -r 0526ade4a23b src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu Aug 20 16:37:18 1998 +0200
+++ b/src/HOL/arith_data.ML	Thu Aug 20 16:44:05 1998 +0200
@@ -230,5 +230,5 @@
 by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
 				      Suc_diff_n]) 1);
 by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [less_imp_diff_is_0]) 1);
+by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
 qed_spec_mp "diff_less_mono2";