# HG changeset patch
# User berghofe
# Date 1064239296 -7200
# Node ID d6cb80cc1d2052646b4073469b785ec4f0fd626d
# Parent  2014eac694d27cd21611e17ff91797bc783d73e4
Improved efficiency of code generated for < predicate on natural numbers.

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