src/Pure/display.ML
changeset 19327 4565e230e6eb
parent 19300 7689f81f8996
child 19365 4fd1246d7998