src/Pure/display.ML
changeset 17339 ab97ccef124a
parent 16937 0822bbdd6769
child 17447 3a23acfdf5ba