src/Pure/General/xml.ML
changeset 22421 51a18dd1ea86
parent 22334 4c96d3370186
equal deleted inserted replaced
22420:4ccc8c1b08a3 22421:51a18dd1ea86