src/Pure/Tools/xml.ML
2007-07-28 wenzelm 2007-07-28 tuned;
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-10 wenzelm 2007-07-10 renamed XML.Rawtext to XML.Output;
2007-07-07 wenzelm 2007-07-07 export attribute;
2007-07-07 wenzelm 2007-07-07 moved General/xml.ML to Tools/xml.ML;