diff -r 9ae89b9ce206 -r 58bd51302b21 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Fri Jul 14 14:47:15 2000 +0200
+++ b/src/HOL/UNITY/Guar.thy	Fri Jul 14 14:51:02 2000 +0200
@@ -38,8 +38,8 @@
   guar :: ['a program set, 'a=>'b, 'a program set] => 'a program set
    ("(_/ guarantees[_]/ _)" [55,0,55] 55)
                               (*higher than membership, lower than Co*)
-   "X guarantees[v] Y == {F. ALL G. G : preserves v --> F Join G : X -->
-		       F Join G : Y}"
+   "X guarantees[v] Y == {F. ALL G : preserves v. 
+                               F Join G : X --> F Join G : Y}"
 
   refines :: ['a program, 'a program, 'a program set] => bool
 			("(3_ refines _ wrt _)" [10,10,10] 10)