src/Pure/General/graph.ML
changeset 31288 67dff9c5b2bd
parent 30290 f49d70426690
child 31516 9801a92d52d7