src/Pure/General/graph_display.ML
changeset 59874 3ecb48ce92d7
parent 59449 6d1221b590eb
child 60089 8bd5999133d4