changeset 35627 | 6cec06ef67a7 |
parent 32566 | e6b66a59bed6 |
child 40747 | 889b7545a408 |
--- a/src/Pure/ML-Systems/proper_int.ML Sun Mar 07 12:47:02 2010 +0100 +++ b/src/Pure/ML-Systems/proper_int.ML Sun Mar 07 15:49:49 2010 +0100 @@ -165,6 +165,15 @@ val fromInt = Word.fromInt o dest_int; end; +structure Word32 = +struct + open Word32; + val wordSize = mk_int Word32.wordSize; + val toInt = mk_int o Word32.toInt; + val toIntX = mk_int o Word32.toIntX; + val fromInt = Word32.fromInt o dest_int; +end; + (* Real *)