src/Pure/display.ML
changeset 12902 a23dc0b7566f
parent 12831 a2a3896f9c48
child 13658 c9ad3e64ddcf