src/Pure/display.ML
changeset 16352 d7f9978e5752
parent 16334 b773132e3715
child 16364 dc9f7066d80a