src/Pure/display.ML
changeset 13049 ce180e5b7fa0
parent 12831 a2a3896f9c48
child 13658 c9ad3e64ddcf