src/HOL/Integ/IntDef.thy

   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
     dest: zless_imp_add1_zle)
 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 ..
 
 consts_code
   "0" :: "int"                       ("0")

 
 *}
 
 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"
 *}
 
 quickcheck_params [default_type = int]