Wed, 11 Jul 2007 17:47:45 +0200 | wenzelm | Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols); | file | diff | annotate |
Tue, 10 Jul 2007 23:29:49 +0200 | wenzelm | renamed XML.Rawtext to XML.Output; | file | diff | annotate |
Sat, 07 Jul 2007 12:16:20 +0200 | wenzelm | export attribute; | file | diff | annotate |
Sat, 07 Jul 2007 00:14:54 +0200 | wenzelm | moved General/xml.ML to Tools/xml.ML; | file | diff | annotate |