src/HOL/Arith_Tools.thy

--- a/src/HOL/Arith_Tools.thy	Fri Dec 05 17:35:22 2008 -0800
+++ b/src/HOL/Arith_Tools.thy	Sat Dec 06 19:39:53 2008 -0800
@@ -40,7 +40,7 @@
 text{*No longer required as a simprule because of the @{text inverse_fold}
    simproc*}
 lemma Suc_diff_number_of:
-     "neg (number_of (uminus v)::int) ==>
+     "Int.Pls < v ==>
       Suc m - (number_of v) = m - (number_of (Int.pred v))"
 apply (subst Suc_diff_eq_diff_pred)
 apply simp