src/Pure/display.ML
changeset 5253 82a5ca6290aa
parent 5245 a6167c446b0b
child 5902 c39b23d752b6