src/Pure/display.ML
changeset 4724 3d2375efb80e
parent 4498 a088ec3e4f5e
child 4782 9c0b31da51c6