src/Pure/display.ML
changeset 29055 edaef19665e6
parent 28840 049f0a8faa35
child 29091 b81fe045e799