# HG changeset patch
# User paulson
# Date 935660358 -7200
# Node ID a979e8a2ee18622ef9a5c4b4d3b2e6ad59e8e608
# Parent  eddb3d77a36316bfb5d63f3227a7a8c7349d04ea
changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE

diff -r eddb3d77a363 -r a979e8a2ee18 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Thu Aug 26 11:37:43 1999 +0200
+++ b/src/HOL/UNITY/Comp.thy	Thu Aug 26 11:39:18 1999 +0200
@@ -34,9 +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 "guar" 65)
-   "X guar Y == {F. ALL H. F component H --> H:X --> H:Y}"
+  guar :: ['a program set, 'a program set] => 'a program set
+   (infixl "guarantees" 55)    (*higher than membership, lower than Co*)
+   "X guarantees 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)