src/Pure/display.ML
changeset 51618 a3577cd80c41
parent 51584 98029ceda8ce
child 52043 286629271d65