src/Pure/PIDE/xml.ML
changeset 62799 46e6f91c4da1
parent 62663 bea354f6ff21
child 62819 d3ff367a16a0
equal deleted inserted replaced
62798:2948681ea85f 62799:46e6f91c4da1