src/Pure/term_xml.ML
changeset 46579 fa035a015ea8
parent 43789 321ebd051897
child 70784 799437173553
equal deleted inserted replaced
46578:1bc7e91a5c77 46579:fa035a015ea8