src/Pure/display.ML
changeset 28741 1b257449f804
parent 28316 b17d863a050f
child 28802 9ba30eeec7ce