src/HOL/Tools/numeral.ML
changeset 37881 096c8397c989
parent 34944 970e1466028d
child 38923 79d7f2b4cf71
equal deleted inserted replaced
37880:3b9ca8d2c5fb 37881:096c8397c989
    75       in dest_num end;
    75       in dest_num end;
    76     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    76     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    77       (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    77       (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    78   in
    78   in
    79     thy |> Code_Target.add_syntax_const target number_of
    79     thy |> Code_Target.add_syntax_const target number_of
    80       (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
    80       (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
    81         @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
    81         @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))))
    82   end;
    82   end;
    83 
    83 
    84 end; (*local*)
    84 end; (*local*)
    85 
    85 
    86 end;
    86 end;