src/Pure/display.ML
changeset 15194 ddbbab501213
parent 15000 3d6245229e48
child 15531 08c8dad8e399