src/Pure/display.ML
changeset 24077 e7ba448bc571
parent 23657 2332c79f4dc8
child 24665 e5bea50b9b89