src/Pure/General/xml.scala
Fri, 04 Dec 2009 14:21:07 +0100 wenzelm added document_node;
Mon, 29 Dec 2008 22:36:56 +0100 wenzelm tuned;
less more (0) -10 -2 tip