src/Pure/display.ML
changeset 3372 6e472c8f0011
parent 2992 395686b418a4
child 3531 f6cc9112f4e9
equal deleted inserted replaced
3371:80f0d0b2f404 3372:6e472c8f0011