src/Pure/display.ML
changeset 26672 f99956db6ccd
parent 26637 0bfccafc52eb
child 26928 ca87aff1ad2d