fix looping simp rule
authorhuffman
Fri, 22 Jun 2007 22:41:17 +0200
changeset 23476 839db6346cc8
parent 23475 c869b52a9077
child 23477 f4b83f03cac9
fix looping simp rule
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)"