src/Pure/PIDE/xml.ML
changeset 63654 f90e3926e627
parent 62819 d3ff367a16a0
child 63806 c54a53ef1873