# 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 */