# HG changeset patch
# User haftmann
# Date 1200901412 -3600
# Node ID db0fd0ecdcd4c0a7696e3a5b95a5a33c2ea32141
# Parent  b1d1ab3e5a2e3e0c969b4fa0a6fb86485cdd6c6b
explicit auxiliary function for code setup

diff -r b1d1ab3e5a2e -r db0fd0ecdcd4 src/HOL/Tools/numeral.ML
--- 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;