# HG changeset patch
# User paulson
# Date 903515197 -7200
# Node ID 68e5eeee4e599784c79c70284f7f863001667e9f
# Parent  ea33e66dceddf9f66c81d5f3a83fe1601cf8b3e5
less_imp_diff_positive is redundant with new simprule zero_less_diff

diff -r ea33e66dcedd -r 68e5eeee4e59 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Wed Aug 19 10:26:02 1998 +0200
+++ b/src/HOL/Divides.ML	Wed Aug 19 10:26:37 1998 +0200
@@ -228,7 +228,6 @@
  by (subgoal_tac "(m-n) div n < (m-n)" 1);
   by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
- by (dres_inst_tac [("m","n")] less_imp_diff_positive 1);
  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
 (* case n=m *)
 by (subgoal_tac "m=n" 1);