src/Pure/display.ML
changeset 55873 aa50d903e0a7
parent 55633 460f4801b5cb
child 56025 d74fed45fa8b