src/Pure/display.ML
changeset 13049 ce180e5b7fa0
parent 12831 a2a3896f9c48
child 13658 c9ad3e64ddcf
equal deleted inserted replaced
13048:8b2eb3b78cc3 13049:ce180e5b7fa0