Added code lemma for <

--- 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 *}