src/Tools/random_word.ML
Sat, 22 Dec 2007 14:10:24 +0100 wenzelm added int/real/list operations;
Thu, 20 Dec 2007 14:33:40 +0100 wenzelm moved Pure/General/random_word.ML to Tools/random_word.ML;
less more (0) tip