src/HOL/Library/Code_Integer.thy
changeset 25928 042e877d9841
parent 25919 8b1c0d434824
child 26009 b6a64fe38634
equal deleted inserted replaced
25927:9c544dac6269 25928:042e877d9841
    22 
    22 
    23 code_instance int :: eq
    23 code_instance int :: eq
    24   (Haskell -)
    24   (Haskell -)
    25 
    25 
    26 setup {*
    26 setup {*
    27   fold (fn target => CodeTarget.add_pretty_numeral target true
    27   fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
    28     @{const_name number_int_inst.number_of_int}
    28     true true) ["SML", "OCaml", "Haskell"]
    29     @{const_name Int.B0} @{const_name Int.B1}
       
    30     @{const_name Int.Pls} @{const_name Int.Min}
       
    31     @{const_name Int.Bit}
       
    32   ) ["SML", "OCaml", "Haskell"]
       
    33 *}
    29 *}
    34 
    30 
    35 code_const "Int.Pls" and "Int.Min" and "Int.Bit"
    31 code_const "Int.Pls" and "Int.Min" and "Int.Bit"
    36   (SML "raise/ Fail/ \"Pls\""
    32   (SML "raise/ Fail/ \"Pls\""
    37      and "raise/ Fail/ \"Min\""
    33      and "raise/ Fail/ \"Min\""