src/Pure/display.ML
changeset 32196 bda40fb76a65
parent 32187 cca43ca13f4f
child 32430 de3727f1cf12
equal deleted inserted replaced
32195:d77476e4040c 32196:bda40fb76a65