src/Pure/term_xml.ML
changeset 81954 6f2bcdfa9a19
parent 80589 7849b6370425