src/Pure/Tools/legacy_xml_syntax.ML
changeset 50456 e732da007562
parent 50217 ce1f0602f48e
equal deleted inserted replaced
50449:75e00ff42870 50456:e732da007562