src/Pure/General/graph.ML
changeset 45023 76abd26e2e2d
parent 44338 700008399ee5
child 46611 669601fa1a62
equal deleted inserted replaced
45022:3c888c58e10b 45023:76abd26e2e2d