src/Pure/General/graph.ML
changeset 27885 76b51cd0a37c
parent 25538 58e8ba3b792b
child 28183 7d5103454520