src/Pure/display.ML
changeset 4550 53553ccda0e6
parent 4498 a088ec3e4f5e
child 4782 9c0b31da51c6