src/HOL/UNITY/Simple/Reachability.thy
changeset 16417 9bc16273c2d4
parent 13806 fd40c9d9076b
child 23767 7272a839ccd9
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     6 Reachability in Graphs
     6 Reachability in Graphs
     7 
     7 
     8 From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
     8 From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
     9 *)
     9 *)
    10 
    10 
    11 theory Reachability = Detects + Reach:
    11 theory Reachability imports Detects Reach begin
    12 
    12 
    13 types  edge = "(vertex*vertex)"
    13 types  edge = "(vertex*vertex)"
    14 
    14 
    15 record state =
    15 record state =
    16   reach :: "vertex => bool"
    16   reach :: "vertex => bool"