# HG changeset patch
# User berghofe
# Date 1008856528 -3600
# Node ID 671b4d632c343d8a664d241dc165f301700eb7bf
# Parent  90ac72455fcc5f3075f0da1fb4b806890c7bfbd3
Declared characteristic equations for < on nat for code generation.

diff -r 90ac72455fcc -r 671b4d632c34 src/HOL/Main.thy
--- 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