src/Pure/General/xml.ML
changeset 38422 f96394dba335
parent 38266 492d377ecfe2
child 38474 e498dc2eb576