src/Pure/display.ML
changeset 26561 394cd765643d
parent 26423 8408edac8f6b
child 26626 c6231d64d264