src/Pure/General/graph.ML
changeset 25995 21b51f748daf
parent 25538 58e8ba3b792b
child 28183 7d5103454520
equal deleted inserted replaced
25994:d35484265f46 25995:21b51f748daf