src/Pure/display.ML
changeset 55144 de95c97efab3
parent 52043 286629271d65
child 55633 460f4801b5cb