src/Pure/display.ML
changeset 19960 a0e3f2df9b0e
parent 19806 f860b7a98445
child 20076 def4ad161528
equal deleted inserted replaced
19959:dc3e007aeaf1 19960:a0e3f2df9b0e