src/Pure/display.ML
changeset 14898 a25550451b51
parent 14876 477c414000f8
child 14990 582b655da757