src/Pure/display.ML
changeset 52014 45929e0e1d73
parent 51584 98029ceda8ce
child 52043 286629271d65