src/Pure/display.ML
changeset 31297 a176e4dfb388
parent 30723 a3adc9a96a16
child 32089 568a23753e3a
equal deleted inserted replaced
31296:ba296a58d813 31297:a176e4dfb388