# HG changeset patch
# User wenzelm
# Date 1507635972 -7200
# Node ID 3b50269b90c2e1c07c74ed5b01762c9380e59a98
# Parent  5baca4c94737a2b828c0eb985546c5fd58a9b915
more operations;

diff -r 5baca4c94737 -r 3b50269b90c2 src/Pure/General/graph.ML
--- 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 *)
 
diff -r 5baca4c94737 -r 3b50269b90c2 src/Pure/General/graph.scala
--- 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 */