explicit auxiliary function for code setup
authorhaftmann
Mon Jan 21 08:43:32 2008 +0100 (2008-01-21)
changeset 25932db0fd0ecdcd4
parent 25931 b1d1ab3e5a2e
child 25933 7fc0f4065251
explicit auxiliary function for code setup
src/HOL/Tools/numeral.ML
     1.1 --- a/src/HOL/Tools/numeral.ML	Mon Jan 21 08:43:31 2008 +0100
     1.2 +++ b/src/HOL/Tools/numeral.ML	Mon Jan 21 08:43:32 2008 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val mk_cnumeral: int -> cterm
     1.6    val mk_cnumber: ctyp -> int -> cterm
     1.7 +  val add_code: string -> bool -> bool -> string -> theory -> theory
     1.8  end;
     1.9  
    1.10  structure Numeral: NUMERAL =
    1.11 @@ -51,4 +52,13 @@
    1.12  
    1.13  end;
    1.14  
    1.15 +
    1.16 +(* code generator *)
    1.17 +
    1.18 +fun add_code number_of negative unbounded target =
    1.19 +  CodeTarget.add_pretty_numeral target unbounded negative number_of
    1.20 +  @{const_name Int.B0} @{const_name Int.B1}
    1.21 +  @{const_name Int.Pls} @{const_name Int.Min}
    1.22 +  @{const_name Int.Bit};
    1.23 +
    1.24  end;