src/Pure/display.ML
changeset 7025 afbd8241797b
parent 6976 3895ba31db71
child 7067 601f930d3739