src/Pure/display.ML
changeset 13292 f504f5d284d3
parent 12831 a2a3896f9c48
child 13658 c9ad3e64ddcf