src/HOL/Main.thy
changeset 14192 d6cb80cc1d20
parent 14102 8af7334af4b3
child 14350 41b32020d0b3
--- 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