src/Pure/PIDE/xml.ML
Sun, 04 Sep 2011 15:21:50 +0200 wenzelm moved XML/YXML to src/Pure/PIDE;
less more (0) tip