src/Pure/PIDE/xml.ML
changeset 69484 ed6b100a9c7d
parent 69345 6bd63c94cf62
child 69574 b4ea943ce0b7
equal deleted inserted replaced
69483:023d92df3d84 69484:ed6b100a9c7d