src/Pure/General/graph_display.ML
changeset 50516 ed6b40d15d1c
parent 50450 358b6020f8b6
child 50715 8cfd585b9162