src/HOL/Library/Code_Integer.thy
changeset 25928 042e877d9841
parent 25919 8b1c0d434824
child 26009 b6a64fe38634
     1.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Jan 18 20:34:28 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Jan 21 08:43:27 2008 +0100
     1.3 @@ -24,12 +24,8 @@
     1.4    (Haskell -)
     1.5  
     1.6  setup {*
     1.7 -  fold (fn target => CodeTarget.add_pretty_numeral target true
     1.8 -    @{const_name number_int_inst.number_of_int}
     1.9 -    @{const_name Int.B0} @{const_name Int.B1}
    1.10 -    @{const_name Int.Pls} @{const_name Int.Min}
    1.11 -    @{const_name Int.Bit}
    1.12 -  ) ["SML", "OCaml", "Haskell"]
    1.13 +  fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
    1.14 +    true true) ["SML", "OCaml", "Haskell"]
    1.15  *}
    1.16  
    1.17  code_const "Int.Pls" and "Int.Min" and "Int.Bit"