author | huffman |
Fri, 22 Jun 2007 22:41:17 +0200 | |
changeset 23476 | 839db6346cc8 |
parent 23475 | c869b52a9077 |
child 23477 | f4b83f03cac9 |
src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |
--- 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)"