src/Pure/display.ML
changeset 17740 fc385ce6187d
parent 17704 f776b3bf4126
child 17995 8b9c6af78a67