src/Pure/General/graph.ML
changeset 33178 70522979c7be
parent 32710 fa46afc8c05f
child 35012 c3e3ac3ca091