src/Pure/display.ML
changeset 25456 6f79698f294d
parent 25405 7ac8c93be624
child 26423 8408edac8f6b