src/Pure/display.ML
changeset 25366 05c2ae18cc51
parent 24920 2a45e400fdad
child 25405 7ac8c93be624