more operations;

--- a/src/Pure/General/graph.ML	Tue Oct 10 11:24:35 2017 +0200
+++ b/src/Pure/General/graph.ML	Tue Oct 10 13:46:12 2017 +0200
@@ -40,6 +40,7 @@
   val maximals: 'a T -> key list
   val is_minimal: 'a T -> key -> bool
   val is_maximal: 'a T -> key -> bool
+  val is_isolated: 'a T -> key -> bool
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
@@ -177,6 +178,8 @@
 fun is_minimal G x = Keys.is_empty (imm_preds G x);
 fun is_maximal G x = Keys.is_empty (imm_succs G x);
 
+fun is_isolated G x = is_minimal G x andalso is_maximal G x;
+
 
 (* node operations *)
 

--- a/src/Pure/General/graph.scala	Tue Oct 10 11:24:35 2017 +0200
+++ b/src/Pure/General/graph.scala	Tue Oct 10 13:46:12 2017 +0200
@@ -147,6 +147,8 @@
   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
 
+  def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
+
 
   /* node operations */