src/Pure/display.ML
changeset 15386 06757406d8cf
parent 15000 3d6245229e48
child 15531 08c8dad8e399