src/Pure/PIDE/xml.ML
changeset 75436 40630fec3b5d
parent 74789 a5c23da73fca
child 80461 38d020af64aa
equal deleted inserted replaced
75435:c8087e6bd2ce 75436:40630fec3b5d