src/Pure/General/graph_display.ML
changeset 50180 c6626861c31a
parent 49570 2265456f6131
child 50201 c26369c9eda6