src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Fri Jun 22 20:19:39 2007 +0200
+++ b/src/HOL/Nat.thy	Fri Jun 22 22:41:17 2007 +0200
@@ -957,7 +957,7 @@
   shows "\<exists>k::nat. 0 < k & i + k = j"
 proof
   from assms show "0 < j - i & i + (j - i) = j"
-    by (simp add: add_diff_inverse less_not_sym)
+    by (simp add: order_less_imp_le)
 qed
 
 lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"