changeset 37853 | 26906cacbaae |
parent 35974 | 3a588b344749 |
child 39020 | ac0f24f850c9 |
--- a/src/Pure/General/graph.ML Tue Jul 20 14:44:33 2010 +0200 +++ b/src/Pure/General/graph.ML Tue Jul 20 16:42:48 2010 +0200 @@ -20,6 +20,7 @@ val minimals: 'a T -> key list val maximals: 'a T -> key list val subgraph: (key -> bool) -> 'a T -> 'a T + val get_entry: 'a T -> key -> 'a * (key list * key list) (*exception UNDEF*) val map_nodes: ('a -> 'b) -> 'a T -> 'b T val get_node: 'a T -> key -> 'a (*exception UNDEF*) val map_node: key -> ('a -> 'a) -> 'a T -> 'a T