diff -r 2014eac694d2 -r d6cb80cc1d20 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Sep 15 17:15:00 2003 +0200
+++ b/src/HOL/Main.thy	Mon Sep 22 16:01:36 2003 +0200
@@ -88,6 +88,7 @@
 setup eq_codegen_setup
 
 lemma [code]: "((n::nat) < 0) = False" by simp
-lemmas [code] = less_Suc_eq imp_conv_disj
+lemma [code]: "(0 < Suc n) = True" by simp
+lemmas [code] = Suc_less_eq imp_conv_disj
 
 end