src/Pure/PIDE/yxml.ML
changeset 74215 7515abfe18cf
parent 73557 225486d9c960
child 74231 b3c65c984210
equal deleted inserted replaced
74214:e16ac8907148 74215:7515abfe18cf