src/HOL/UNITY/Comp.thy
changeset 7364 a979e8a2ee18
parent 6822 8932f33259d4
child 7399 cf780c2bcccf
     1.1 --- a/src/HOL/UNITY/Comp.thy	Thu Aug 26 11:37:43 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Thu Aug 26 11:39:18 1999 +0200
     1.3 @@ -34,9 +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
     1.8 -                                                    (infixl "guar" 65)
     1.9 -   "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"
    1.10 +  guar :: ['a program set, 'a program set] => 'a program set
    1.11 +   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
    1.12 +   "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
    1.13  
    1.14    refines :: ['a program, 'a program, 'a program set] => bool
    1.15  			("(3_ refines _ wrt _)" [10,10,10] 10)