src/Pure/display.ML
changeset 8341 8f0f0ae02b10
parent 7635 4c1d2eb68db8
child 8402 84ff2d1f9a2c