src/Pure/display.ML
changeset 52344 ff05e50efa0d
parent 52043 286629271d65
child 55633 460f4801b5cb