Sun, 08 Nov 2009 13:56:44 +0100 | wenzelm | modernized structure Random_Word; | file | diff | annotate |
Tue, 29 Sep 2009 16:24:36 +0200 | wenzelm | explicit indication of Unsynchronized.ref; | file | diff | annotate |
Sat, 28 Feb 2009 14:09:58 +0100 | wenzelm | removed Ids; | file | diff | annotate |
Sat, 22 Dec 2007 14:10:24 +0100 | wenzelm | added int/real/list operations; | file | diff | annotate |
Thu, 20 Dec 2007 14:33:40 +0100 | wenzelm | moved Pure/General/random_word.ML to Tools/random_word.ML; | file | diff | annotate |