src/Pure/display.ML
changeset 16843 8ff9a80f3c93
parent 16534 95460b6eb712
child 16845 bedf7b5fb781
equal deleted inserted replaced
16842:5979c46853d1 16843:8ff9a80f3c93