changeset 25145 | d432105e5bd0 |
parent 25089 | 04b8456f7754 |
child 25491 | 5760991891dd |
--- 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)