src/Pure/General/xml.ML
changeset 39121 6f6a9c8abbac
parent 38474 e498dc2eb576
child 39555 ccb223a4d49c
equal deleted inserted replaced
39104:7430f17fd80e 39121:6f6a9c8abbac