src/Pure/display.ML
changeset 28337 93964076e7b8
parent 28316 b17d863a050f
child 28802 9ba30eeec7ce
equal deleted inserted replaced
28336:a8edf4c69a79 28337:93964076e7b8