src/Pure/display.ML
changeset 52516 b5b3c888df9f
parent 52043 286629271d65
child 55633 460f4801b5cb