src/Pure/term_xml.ML
changeset 65855 33b3e76114f8
parent 43789 321ebd051897
child 70784 799437173553
equal deleted inserted replaced
65854:db070951dfee 65855:33b3e76114f8