src/Pure/General/xml.ML
changeset 38286 c9c7bd836894
parent 38228 ada3ab6b9085
child 38266 492d377ecfe2