src/Pure/display.ML
changeset 2160 ad4382e546fc
parent 1591 7fa0265dcd13
child 2180 934572a94139
equal deleted inserted replaced
2159:e650a3f6f600 2160:ad4382e546fc