src/HOL/UNITY/Comp.thy
changeset 6822 8932f33259d4
parent 6646 3ea726909fff
child 7364 a979e8a2ee18
     1.1 --- a/src/HOL/UNITY/Comp.thy	Sun Jun 13 13:52:26 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Sun Jun 13 13:52:50 1999 +0200
     1.3 @@ -34,8 +34,9 @@
     1.4    component :: ['a program, 'a program] => bool     (infixl 50)
     1.5     "F component H == EX G. F Join G = H"
     1.6  
     1.7 -  guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
     1.8 -   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
     1.9 +  guarantees :: ['a program set, 'a program set] => 'a program set
    1.10 +                                                    (infixl "guar" 65)
    1.11 +   "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"
    1.12  
    1.13    refines :: ['a program, 'a program, 'a program set] => bool
    1.14  			("(3_ refines _ wrt _)" [10,10,10] 10)