src/Pure/display.ML
changeset 14722 8e739a6eaf11
parent 14644 3224082514f9
child 14794 751d5af6d91e