src/Pure/General/graph.ML
changeset 48732 f04320479ff9
parent 48350 09bf3b73e446
child 49560 11430dd89e35
equal deleted inserted replaced
48731:a45ba78abcc1 48732:f04320479ff9