src/Pure/display.ML
changeset 14360 e654599b114e
parent 14223 0ee05eef881b
child 14472 cba7c0a3ffb3