more operations;
authorwenzelm
Tue Oct 10 13:46:12 2017 +0200 (19 months ago)
changeset 668303b50269b90c2
parent 66829 5baca4c94737
child 66831 29ea2b900a05
more operations;
src/Pure/General/graph.ML
src/Pure/General/graph.scala
     1.1 --- a/src/Pure/General/graph.ML	Tue Oct 10 11:24:35 2017 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Tue Oct 10 13:46:12 2017 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4    val maximals: 'a T -> key list
     1.5    val is_minimal: 'a T -> key -> bool
     1.6    val is_maximal: 'a T -> key -> bool
     1.7 +  val is_isolated: 'a T -> key -> bool
     1.8    val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
     1.9    val default_node: key * 'a -> 'a T -> 'a T
    1.10    val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
    1.11 @@ -177,6 +178,8 @@
    1.12  fun is_minimal G x = Keys.is_empty (imm_preds G x);
    1.13  fun is_maximal G x = Keys.is_empty (imm_succs G x);
    1.14  
    1.15 +fun is_isolated G x = is_minimal G x andalso is_maximal G x;
    1.16 +
    1.17  
    1.18  (* node operations *)
    1.19  
     2.1 --- a/src/Pure/General/graph.scala	Tue Oct 10 11:24:35 2017 +0200
     2.2 +++ b/src/Pure/General/graph.scala	Tue Oct 10 13:46:12 2017 +0200
     2.3 @@ -147,6 +147,8 @@
     2.4    def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
     2.5    def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
     2.6  
     2.7 +  def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
     2.8 +
     2.9  
    2.10    /* node operations */
    2.11