src/HOL/UNITY/Union.thy
changeset 7915 c7fd7eb3b0ef
parent 7878 43b03d412b82
child 7947 b999c1ab9327
     1.1 --- a/src/HOL/UNITY/Union.thy	Fri Oct 22 18:33:39 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Fri Oct 22 18:35:20 1999 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  
     1.5    (*The weak version of localTo, considering only G's reachable states*)
     1.6    LocalTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
     1.7 -    "v LocalTo F == {G. G : v localTo[reachable G] F}"
     1.8 +    "v LocalTo F == {G. G : v localTo[reachable (F Join G)] F}"
     1.9  
    1.10    (*Two programs with disjoint actions, except for identity actions.
    1.11      It's a weak property but still useful.*)