src/Pure/General/graph.ML
changeset 33049 c38f02fdf35d
parent 32710 fa46afc8c05f
child 35012 c3e3ac3ca091