src/Pure/term_xml.ML
changeset 51405 2aea76fe9c73
parent 43789 321ebd051897
child 70784 799437173553
equal deleted inserted replaced
51396:f4c82c165f58 51405:2aea76fe9c73