src/Pure/General/graph.ML
changeset 48583 ed975dbb16ca
parent 48350 09bf3b73e446
child 49560 11430dd89e35
equal deleted inserted replaced
48582:c6bed330fc07 48583:ed975dbb16ca