# HG changeset patch
# User huffman
# Date 1182544877 -7200
# Node ID 839db6346cc844c3c52f005c56164ea786fb4be2
# Parent  c869b52a9077500623842f0fbba6a9f9bc44aa2c
fix looping simp rule

diff -r c869b52a9077 -r 839db6346cc8 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)"