src/Pure/PIDE/yxml.ML
changeset 78842 eb572f7b6689
parent 77768 65008644d394
child 80504 7ea69c26524b
equal deleted inserted replaced
78841:7f61688d4e8d 78842:eb572f7b6689