src/Pure/General/graph.ML
changeset 19761 5cd82054c2c6
parent 19615 e3ab6cd838a4
child 19950 fd74bf4e603e