src/Pure/PIDE/xml.ML
changeset 45666 d83797ef0d2d
parent 45155 3216d65d8f34
child 46837 5bdd68f380b3
equal deleted inserted replaced
45665:129db1416717 45666:d83797ef0d2d