src/Pure/General/graph.ML
changeset 28154 3c3663e24ba7
parent 25538 58e8ba3b792b
child 28183 7d5103454520
equal deleted inserted replaced
28153:67147cc3f967 28154:3c3663e24ba7