src/Pure/term_xml.ML
changeset 59119 c90c02940964
parent 43789 321ebd051897
child 70784 799437173553
equal deleted inserted replaced
59118:fe7f91f85789 59119:c90c02940964