src/Pure/General/graph.ML
changeset 38422 f96394dba335
parent 37853 26906cacbaae
child 39020 ac0f24f850c9