src/Pure/General/xml.ML
changeset 26336 a0e2b706ce73
parent 25838 00b2a1b2c4e9
child 26525 14a56f013469
equal deleted inserted replaced
26335:961bbcc9d85b 26336:a0e2b706ce73