src/Pure/term_xml.ML
changeset 64068 3a506cb576d3
parent 43789 321ebd051897
child 70784 799437173553
equal deleted inserted replaced
64067:6855c2f7aa6a 64068:3a506cb576d3