src/Pure/General/graph.ML
changeset 48542 0a5f598cacec
parent 48350 09bf3b73e446
child 49560 11430dd89e35