src/Pure/General/graph.ML
changeset 18208 dbdcf366db53
parent 18133 1d403623dabc
child 18921 f47c46d7d654
equal deleted inserted replaced
18207:9edbeda7e39a 18208:dbdcf366db53