src/Pure/display.ML
changeset 50210 747db833fbf7
parent 50126 3dec88149176
child 50301 56b4c9afd7be
equal deleted inserted replaced
50209:907373a080b9 50210:747db833fbf7