diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/UNITY/Guar.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,19 +1,13 @@
 (*  Title:      HOL/UNITY/Guar.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1999  University of Cambridge
+    Author:     Sidi Ehmety
 
 From Chandy and Sanders, "Reasoning About Program Composition",
 Technical Report 2000-003, University of Florida, 2000.
 
-Revised by Sidi Ehmety on January 2001
-
-Added: Compatibility, weakest guarantees, etc.
-
-and Weakest existential property,
-from Charpentier and Chandy "Theorems about Composition",
+Compatibility, weakest guarantees, etc.  and Weakest existential
+property, from Charpentier and Chandy "Theorems about Composition",
 Fifth International Conference on Mathematics of Program, 2000.
-
 *)
 
 header{*Guarantees Specifications*}
@@ -66,7 +60,7 @@
   "welldef == {F. Init F \<noteq> {}}"
   
   refines :: "['a program, 'a program, 'a program set] => bool"
-			("(3_ refines _ wrt _)" [10,10,10] 10)
+                        ("(3_ refines _ wrt _)" [10,10,10] 10)
   "G refines F wrt X ==
      \<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> 
          (G\<squnion>H \<in> welldef \<inter> X)"