src/Pure/ML-Systems/proper_int.ML
changeset 43948 8f5add916a99
parent 42017 0d4bedb25fc9
child 45030 9cf265a192f6
equal deleted inserted replaced
43947:9b00f09f7721 43948:8f5add916a99
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 SML basis with type int representing proper integers, not machine
     4 SML basis with type int representing proper integers, not machine
     5 words.
     5 words.
     6 *)
     6 *)
     7 
       
     8 val ml_system_fix_ints = true;
       
     9 
     7 
    10 val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
     8 val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
    11 val dest_int = IntInf.toInt: IntInf.int -> Int.int;
     9 val dest_int = IntInf.toInt: IntInf.int -> Int.int;
    12 
    10 
    13 
    11