src/Pure/General/graph_display.ML
changeset 50126 3dec88149176
parent 49570 2265456f6131
child 50201 c26369c9eda6