src/Tools/random_word.ML
2009-11-08 wenzelm 2009-11-08 modernized structure Random_Word;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-02-28 wenzelm 2009-02-28 removed Ids;
2007-12-22 wenzelm 2007-12-22 added int/real/list operations; tuned interface; tuned;
2007-12-20 wenzelm 2007-12-20 moved Pure/General/random_word.ML to Tools/random_word.ML;