src/Pure/General/xml.ML
changeset 25898 d8f17d8cf9d4
parent 25838 00b2a1b2c4e9
child 26525 14a56f013469
equal deleted inserted replaced
25897:e9d45709bece 25898:d8f17d8cf9d4