src/Pure/term_xml.ML
changeset 81229 e18600daa904
parent 80589 7849b6370425