# HG changeset patch
# User haftmann
# Date 1193064890 -7200
# Node ID d432105e5bd00cc28cfe8568d50cbb4a771d1e19
# Parent  5157a76559b6f8639b025981b73e89273888a4d1
dropped superfluous inlining lemmas

diff -r 5157a76559b6 -r d432105e5bd0 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Oct 22 15:27:11 2007 +0200
+++ b/src/HOL/Nat.thy	Mon Oct 22 16:54:50 2007 +0200
@@ -1129,23 +1129,20 @@
 
 subsection {* Code generator setup *}
 
-lemma one_is_Suc_zero [code inline]: "1 = Suc 0"
-by simp
-
 instance nat :: eq ..
 
 lemma [code func]:
-    "(0\<Colon>nat) = 0 \<longleftrightarrow> True"
-    "Suc n = Suc m \<longleftrightarrow> n = m"
-    "Suc n = 0 \<longleftrightarrow> False"
-    "0 = Suc m \<longleftrightarrow> False"
-by auto
+  "(0\<Colon>nat) = 0 \<longleftrightarrow> True"
+  "Suc n = Suc m \<longleftrightarrow> n = m"
+  "Suc n = 0 \<longleftrightarrow> False"
+  "0 = Suc m \<longleftrightarrow> False"
+  by auto
 
 lemma [code func]:
-    "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
-    "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
-    "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
-    "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
+  "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
+  "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
+  "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
+  "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
   using Suc_le_eq less_Suc_eq_le by simp_all
 
 
diff -r 5157a76559b6 -r d432105e5bd0 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Mon Oct 22 15:27:11 2007 +0200
+++ b/src/HOL/Numeral.thy	Mon Oct 22 16:54:50 2007 +0200
@@ -587,7 +587,7 @@
   "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
   by (simp add: int_aux_def)+
 
-lemma [code unfold]:
+lemma [code, code unfold, code inline del]:
   "int n = int_aux n 0"
   by (simp add: int_aux_def)