src/Pure/display.ML
changeset 19575 2d9940cd52d3
parent 19521 cfdab6a91332
child 19591 e7036e812702