src/Pure/Tools/xml.ML
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