src/Pure/General/graph.scala
Fri, 24 Feb 2012 21:36:20 +0100 wenzelm tuned signature;
Thu, 23 Feb 2012 19:35:05 +0100 wenzelm tuned -- avoid copy of empty value;
Thu, 23 Feb 2012 16:02:07 +0100 wenzelm tuned;
Thu, 23 Feb 2012 15:49:40 +0100 wenzelm clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
Thu, 23 Feb 2012 15:15:59 +0100 wenzelm further graph operations from ML;
Thu, 23 Feb 2012 14:17:51 +0100 wenzelm directed graphs (in Scala);
less more (0) tip