src/Pure/General/graph.ML
changeset 45107 76fef3e57004
parent 44338 700008399ee5
child 46611 669601fa1a62