src/Pure/PIDE/yxml.ML
Wed, 07 Mar 2012 23:21:24 +0100 wenzelm tuned message (cf. ML version);
Wed, 07 Mar 2012 20:49:18 +0100 wenzelm eliminated dead code;
Sun, 04 Sep 2011 15:21:50 +0200 wenzelm moved XML/YXML to src/Pure/PIDE;
less more (0) tip