src/Pure/ML-Systems/proper_int.ML
changeset 24597 cbf2c5cf335e
parent 24140 0683a2fc4041
child 24604 d5c5d2e13fbf
equal deleted inserted replaced
24596:f1333a841b26 24597:cbf2c5cf335e
     3     Author:     Makarius
     3     Author:     Makarius
     4 
     4 
     5 SML basis with type int representing proper integers, not machine
     5 SML basis with type int representing proper integers, not machine
     6 words.
     6 words.
     7 *)
     7 *)
       
     8 
       
     9 val ml_system_fix_ints = true;
     8 
    10 
     9 val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
    11 val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
    10 val dest_int = IntInf.toInt: IntInf.int -> Int.int;
    12 val dest_int = IntInf.toInt: IntInf.int -> Int.int;
    11 
    13 
    12 
    14