src/Pure/General/graph.ML
changeset 69592 a80d8ec6c998
parent 66830 3b50269b90c2
child 70610 d14ddb1df52c
equal deleted inserted replaced
69591:cc6a21413f8a 69592:a80d8ec6c998