src/HOL/UNITY/Traces.thy
changeset 4837 eab729051897
parent 4776 1f9362e769c1
child 5111 8f4b72f0c15d
equal deleted inserted replaced
4836:fc5773ae2790 4837:eab729051897
    13 
    13 
    14 consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
    14 consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
    15 
    15 
    16 inductive "reachable Init Acts"
    16 inductive "reachable Init Acts"
    17   intrs 
    17   intrs 
    18          (*Initial trace is empty*)
       
    19     Init  "s: Init ==> s : reachable Init Acts"
    18     Init  "s: Init ==> s : reachable Init Acts"
    20 
    19 
    21     Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
    20     Acts  "[| act: Acts;  s : reachable Init Acts;  (s,s'): act |]
    22 	   ==> s' : reachable Init Acts"
    21 	   ==> s' : reachable Init Acts"
    23 
    22