--- 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 *)