src/Pure/display.ML
changeset 24547 64c20ee76bc1
parent 23657 2332c79f4dc8
child 24665 e5bea50b9b89