src/Pure/General/graph.scala
2012-02-27 wenzelm 2012-02-27 prefer final ADTs -- prevent ooddities;
2012-02-25 wenzelm 2012-02-25 tuned comments;
2012-02-25 wenzelm 2012-02-25 standard Graph instances;
2012-02-25 wenzelm 2012-02-25 clarified signature -- avoid oddities of Iterable like Iterator.map; specific toString;
2012-02-24 wenzelm 2012-02-24 prefer sorted Map/Set for canonical order of results -- pass ordering via fresh copy of empty; discontinued map_nodes, del_nodes conveniences -- avoid inefficient mapValues wrapper (this is not Table.map from ML); tuned signature;
2012-02-24 wenzelm 2012-02-24 tuned signature;
2012-02-23 wenzelm 2012-02-23 tuned -- avoid copy of empty value;
2012-02-23 wenzelm 2012-02-23 tuned;
2012-02-23 wenzelm 2012-02-23 clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
2012-02-23 wenzelm 2012-02-23 further graph operations from ML;
2012-02-23 wenzelm 2012-02-23 directed graphs (in Scala);