src/Pure/display.ML
changeset 27803 c08f4ea29b83
parent 27302 8d12ac6a3e1c
child 28288 09c812966e7f