changeset 30240 | 5b25fee0362c |
parent 25742 | 1051ef9d87c4 |
child 32740 | 9dd0a2f83429 |
30239:179ff9cb160b | 30240:5b25fee0362c |
---|---|
1 (* Title: Tools/random_word.ML |
1 (* Title: Tools/random_word.ML |
2 ID: $Id$ |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 Simple generator for pseudo-random numbers, using unboxed word |
4 Simple generator for pseudo-random numbers, using unboxed word |
6 arithmetic only. Unprotected concurrency introduces some true |
5 arithmetic only. Unprotected concurrency introduces some true |
7 randomness. |
6 randomness. |