# HG changeset patch
# User berghofe
# Date 1118050257 -7200
# Node ID cd7a83dae4f95655250c1e34c6765b510f886587
# Parent  97c9f2c1de3dc08c28ddc4ae1f451ecc65187f56
Added code lemma for <

diff -r 97c9f2c1de3d -r cd7a83dae4f9 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Mon Jun 06 10:21:53 2005 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Mon Jun 06 11:30:57 2005 +0200
@@ -65,6 +65,8 @@
   by (simp add: zdiv_int [symmetric])
 lemma [code]: "m mod n = nat (int m mod int n)"
   by (simp add: zmod_int [symmetric])
+lemma [code]: "(m < n) = (int m < int n)"
+  by simp
 
 subsection {* Preprocessors *}