src/Pure/General/graph.ML
changeset 48732 f04320479ff9
parent 48350 09bf3b73e446
child 49560 11430dd89e35