src/Pure/PIDE/yxml.ML
changeset 67405 e9ab4ad7bd15
parent 64275 ac2abc987cf9
child 68228 326f4bcc5abc
equal deleted inserted replaced
67404:e128ab544996 67405:e9ab4ad7bd15