equal
deleted
inserted
replaced
6 randomness. |
6 randomness. |
7 *) |
7 *) |
8 |
8 |
9 structure Random :> Random = |
9 structure Random :> Random = |
10 struct |
10 struct |
11 |
|
12 (* MODIFIED by Jasmin Blanchette *) |
|
13 fun CRITICAL e = NAMED_CRITICAL "metis" e; |
|
14 |
11 |
15 (* random words: 0w0 <= result <= max_word *) |
12 (* random words: 0w0 <= result <= max_word *) |
16 |
13 |
17 (*minimum length of unboxed words on all supported ML platforms*) |
14 (*minimum length of unboxed words on all supported ML platforms*) |
18 val _ = Word.wordSize >= 30 |
15 val _ = Word.wordSize >= 30 |