src/Pure/display.ML
changeset 14712 81362115cedd
parent 14644 3224082514f9
child 14794 751d5af6d91e