src/Pure/General/xml.ML
changeset 28904 3ef9489eeef5
parent 28033 f03b5856f286
child 29325 a205acc94356