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