src/Pure/display.ML
changeset 4023 a9dc0484c903
parent 3990 a8c80f5fdd16
child 4126 c41846a38e20