src/HOL/UNITY/Comp.thy
changeset 6646 3ea726909fff
parent 6295 351b3c2b0d83
child 6822 8932f33259d4
     1.1 --- a/src/HOL/UNITY/Comp.thy	Mon May 17 10:37:07 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Mon May 17 10:38:08 1999 +0200
     1.3 @@ -31,11 +31,11 @@
     1.4    welldef :: 'a program set  
     1.5     "welldef == {F. Init F ~= {}}"
     1.6  
     1.7 -  component :: ['a program, 'a program] => bool
     1.8 -   "component F H == EX G. F Join G = H"
     1.9 +  component :: ['a program, 'a program] => bool     (infixl 50)
    1.10 +   "F component H == EX G. F Join G = H"
    1.11  
    1.12    guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
    1.13 -   "X guarantees Y == {F. ALL H. component F H --> H:X --> H:Y}"
    1.14 +   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
    1.15  
    1.16    refines :: ['a program, 'a program, 'a program set] => bool
    1.17  			("(3_ refines _ wrt _)" [10,10,10] 10)