src/Pure/General/random_word.ML
Wed, 19 Dec 2007 23:49:28 +0100 wenzelm tuned comments;
Wed, 19 Dec 2007 23:42:20 +0100 wenzelm tuned RandomWord signature;
Wed, 19 Dec 2007 23:06:14 +0100 wenzelm Simple generator for pseudo-random numbers, using unboxed word arithmetic only.
less more (0) tip