src/Pure/General/graph_display.ML
changeset 49685 4341e4d86872
parent 49570 2265456f6131
child 50201 c26369c9eda6
equal deleted inserted replaced
49684:1cf810b8f600 49685:4341e4d86872