src/Pure/ML-Systems/proper_int.ML
changeset 35627 6cec06ef67a7
parent 32566 e6b66a59bed6
child 40747 889b7545a408
equal deleted inserted replaced
35626:06197484c6ad 35627:6cec06ef67a7
   163   val toInt = mk_int o Word.toInt;
   163   val toInt = mk_int o Word.toInt;
   164   val toIntX = mk_int o Word.toIntX;
   164   val toIntX = mk_int o Word.toIntX;
   165   val fromInt = Word.fromInt o dest_int;
   165   val fromInt = Word.fromInt o dest_int;
   166 end;
   166 end;
   167 
   167 
       
   168 structure Word32 =
       
   169 struct
       
   170   open Word32;
       
   171   val wordSize = mk_int Word32.wordSize;
       
   172   val toInt = mk_int o Word32.toInt;
       
   173   val toIntX = mk_int o Word32.toIntX;
       
   174   val fromInt = Word32.fromInt o dest_int;
       
   175 end;
       
   176 
   168 
   177 
   169 (* Real *)
   178 (* Real *)
   170 
   179 
   171 structure Real =
   180 structure Real =
   172 struct
   181 struct