src/HOL/UNITY/Constrains.thy
changeset 6575 70d758762c50
parent 6570 a7d7985050a9
child 6705 b2662096ccd0
     1.1 --- a/src/HOL/UNITY/Constrains.thy	Tue May 04 13:32:53 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.thy	Tue May 04 13:47:28 1999 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  defs
     1.6    Constrains_def
     1.7 -    "A Co B == {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
     1.8 +    "A Co B == {F. F : (reachable F Int A)  co  B}"
     1.9  
    1.10    Unless_def
    1.11      "A Unless B == (A-B) Co (A Un B)"