src/Pure/PIDE/xml.ML
changeset 60610 f52b4b0c10c4
parent 58854 b979c781c2db
child 60982 67e389f67073
equal deleted inserted replaced
60609:15620ae824c0 60610:f52b4b0c10c4