Declared characteristic equations for < on nat for code generation.

--- a/src/HOL/Main.thy	Wed Dec 19 13:21:12 2001 +0100
+++ b/src/HOL/Main.thy	Thu Dec 20 14:55:28 2001 +0100
@@ -116,4 +116,7 @@
   "Nil"     ("[]")
   "Cons"    ("(_ ::/ _)")
 
+lemma [code]: "((n::nat) < 0) = False" by simp
+declare less_Suc_eq [code]
+
 end