src/Pure/General/graph.ML
changeset 19484 89484a62184a
parent 19482 9f11af8f7ef9
child 19580 c878a09fb849