author | wenzelm |
Thu, 11 Nov 2010 13:07:41 +0100 | |
changeset 40476 | 515eab39b6c2 |
parent 39443 | e330437cd22a |
permissions | -rw-r--r-- |
39348 | 1 |
(* Title: Tools/random_word.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Simple generator for pseudo-random numbers, using unboxed word |
|
5 |
arithmetic only. Unprotected concurrency introduces some true |
|
6 |
randomness. |
|
7 |
*) |
|
8 |
||
9 |
signature Random = |
|
10 |
sig |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
11 |
|
39348 | 12 |
val nextWord : unit -> word |
13 |
||
14 |
val nextBool : unit -> bool |
|
15 |
||
16 |
val nextInt : int -> int (* k -> [0,k) *) |
|
17 |
||
18 |
val nextReal : unit -> real (* () -> [0,1) *) |
|
19 |
||
20 |
end; |