added graph operations for transitive closure and reduction in Scala -- unproven and thus better left out of the kernel-relevant ML module;

--- a/src/Pure/General/graph.scala	Sat Dec 08 22:41:39 2012 +0100
+++ b/src/Pure/General/graph.scala	Sun Dec 09 14:01:09 2012 +0100
@@ -222,6 +222,34 @@
   }
 
 
+  /* transitive closure and reduction */
+
+  def transitive_closure: Graph[Key, A] =
+  {
+    var graph = this
+    for {
+      (_, (_, (preds, succs))) <- this.entries
+      x <- preds
+      y <- succs
+    } graph = graph.add_edge(x, y)
+    graph
+  }
+
+  def transitive_reduction_acyclic: Graph[Key, A] =
+  {
+    val trans = this.transitive_closure
+    assert(!trans.entries.exists({ case (x, (_, (_, succs))) => succs.contains(x) }))
+
+    var graph = this
+    for {
+      (x, (_, (_, succs))) <- this.entries
+      y <- succs
+      if trans.imm_preds(y).exists(z => trans.is_edge(x, z))
+    } graph = graph.del_edge(x, y)
+    graph
+  }
+
+
   /* maintain acyclic graphs */
 
   def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] =