src/Pure/PIDE/xml.ML
changeset 76870 c6cdf2a641f4
parent 74789 a5c23da73fca
child 80461 38d020af64aa
equal deleted inserted replaced
76869:9ed58e165110 76870:c6cdf2a641f4