src/Pure/PIDE/xml.ML
changeset 59199 cb8e5f7a5e4a
parent 58854 b979c781c2db
child 60982 67e389f67073
equal deleted inserted replaced
59198:c73933e07c03 59199:cb8e5f7a5e4a