src/Pure/display.ML
changeset 20818 cb7ec413f95d
parent 20629 8f6cc81ba4a3
child 21646 c07b5b0e8492