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