--- a/src/HOL/Tools/numeral.ML Mon Jan 21 08:43:31 2008 +0100
+++ b/src/HOL/Tools/numeral.ML Mon Jan 21 08:43:32 2008 +0100
@@ -9,6 +9,7 @@
sig
val mk_cnumeral: int -> cterm
val mk_cnumber: ctyp -> int -> cterm
+ val add_code: string -> bool -> bool -> string -> theory -> theory
end;
structure Numeral: NUMERAL =
@@ -51,4 +52,13 @@
end;
+
+(* code generator *)
+
+fun add_code number_of negative unbounded target =
+ CodeTarget.add_pretty_numeral target unbounded negative number_of
+ @{const_name Int.B0} @{const_name Int.B1}
+ @{const_name Int.Pls} @{const_name Int.Min}
+ @{const_name Int.Bit};
+
end;