src/Pure/display.ML
changeset 14706 71590b7733b7
parent 14644 3224082514f9
child 14794 751d5af6d91e