src/Pure/display.ML
changeset 4850 050481f41e28
parent 4782 9c0b31da51c6
child 4950 226f2cde9f4d