src/Pure/General/graph.ML
changeset 69482 186b03abb764
parent 66830 3b50269b90c2
child 70610 d14ddb1df52c
equal deleted inserted replaced
69481:3b89c6b723a2 69482:186b03abb764