src/Pure/General/graph.ML
changeset 40650 d40b347d5b0b
parent 39021 139aada5caf8
child 43792 d5803c3d537a
equal deleted inserted replaced
40649:dc1b5aa908ff 40650:d40b347d5b0b