src/Pure/term_xml.ML
changeset 62459 7a5d88dd8cc9
parent 43789 321ebd051897
child 70784 799437173553
equal deleted inserted replaced
62456:11e06f5283bc 62459:7a5d88dd8cc9