src/Pure/General/graph.ML
changeset 39083 e46acc0ea1fe
parent 37853 26906cacbaae
child 39020 ac0f24f850c9