--- a/src/HOL/UNITY/Comp.thy Sun Jun 13 13:52:26 1999 +0200
+++ b/src/HOL/UNITY/Comp.thy Sun Jun 13 13:52:50 1999 +0200
@@ -34,8 +34,9 @@
component :: ['a program, 'a program] => bool (infixl 50)
"F component H == EX G. F Join G = H"
- guarantees :: ['a program set, 'a program set] => 'a program set (infixl 65)
- "X guarantees Y == {F. ALL H. F component H --> H:X --> H:Y}"
+ guarantees :: ['a program set, 'a program set] => 'a program set
+ (infixl "guar" 65)
+ "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"
refines :: ['a program, 'a program, 'a program set] => bool
("(3_ refines _ wrt _)" [10,10,10] 10)