src/Pure/General/yxml.ML
Wed, 16 Apr 2008 17:40:40 +0200 wenzelm tuned;
Thu, 03 Apr 2008 21:23:38 +0200 wenzelm tuned comments;
Thu, 03 Apr 2008 18:42:38 +0200 wenzelm replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
Thu, 03 Apr 2008 16:03:59 +0200 wenzelm Why XML notation?
less more (0) tip