src/Pure/display.ML
changeset 5543 f457121ff50c
parent 5245 a6167c446b0b
child 5902 c39b23d752b6
equal deleted inserted replaced
5542:f0c303f53730 5543:f457121ff50c