src/Pure/General/graph.scala
changeset 66830 3b50269b90c2
parent 64370 865b39487b5d
child 67012 671decd2e627
     1.1 --- a/src/Pure/General/graph.scala	Tue Oct 10 11:24:35 2017 +0200
     1.2 +++ b/src/Pure/General/graph.scala	Tue Oct 10 13:46:12 2017 +0200
     1.3 @@ -147,6 +147,8 @@
     1.4    def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
     1.5    def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
     1.6  
     1.7 +  def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
     1.8 +
     1.9  
    1.10    /* node operations */
    1.11