src/Pure/PIDE/xml.ML
Sun, 18 Oct 2015 21:30:01 +0200 wenzelm tuned signature;
less more (0) -10 -1 tip