diff -r f8e7c71926e4 -r 454f4be984b7 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Wed Jul 12 00:34:54 2006 +0200 +++ b/src/HOL/Integ/IntDef.thy Wed Jul 12 17:00:22 2006 +0200 @@ -888,7 +888,7 @@ lemma [code]: "nat i = nat_aux 0 i" by (simp add: nat_aux_def) -lemma [code unfolt]: +lemma [code inline]: "neg k = (k < 0)" unfolding neg_def .. @@ -959,9 +959,7 @@ setup {* Codegen.add_codegen "number_of_codegen" number_of_codegen - #> CodegenPackage.add_appconst - ("Numeral.number_of", ((1, 1), - appgen_number)) + (* #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number) *) #> CodegenPackage.set_int_tyco "IntDef.int" *}