src/HOL/UNITY/Union.thy
changeset 7826 c6a8b73b6c2a
parent 7359 98a2afab3f86
child 7878 43b03d412b82
     1.1 --- a/src/HOL/UNITY/Union.thy	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -29,7 +29,8 @@
     1.4    localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
     1.5      "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
     1.6  
     1.7 -  (*Two programs with disjoint actions, except for identity actions *)
     1.8 +  (*Two programs with disjoint actions, except for identity actions.
     1.9 +    It's a weak property but still useful.*)
    1.10    Disjoint :: ['a program, 'a program] => bool
    1.11      "Disjoint F G == Acts F Int Acts G <= {Id}"
    1.12