src/Pure/display.ML
changeset 2183 8d42a7bccf0b
parent 2180 934572a94139
child 2226 f3c6a22681b1