src/Pure/display.ML
changeset 51862 b9a8c3b92a62
parent 51584 98029ceda8ce
child 52043 286629271d65