src/Pure/term_xml.ML
changeset 80712 05b16602a683
parent 80589 7849b6370425