src/Pure/display.ML
changeset 10331 7411e4659d4a
parent 10010 f6ccb6df9cb9
child 10737 c130eb1e863f
equal deleted inserted replaced
10330:4362e906b745 10331:7411e4659d4a