diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/UNITY/Comp.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,16 +1,11 @@
 (*  Title:      HOL/UNITY/Comp.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
+    Author:     Sidi Ehmety
 
-Composition
+Composition.
+
 From Chandy and Sanders, "Reasoning About Program Composition",
 Technical Report 2000-003, University of Florida, 2000.
-
-Revised by Sidi Ehmety on January  2001
-
-Added: a strong form of the \<subseteq> relation (component_of) and localize
-
 *)
 
 header{*Composition: Basic Primitives*}
@@ -46,7 +41,7 @@
 
   localize  :: "('a=>'b) => 'a program => 'a program"
   "localize v F == mk_program(Init F, Acts F,
-			      AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
+                              AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
 
   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
   "funPair f g == %x. (f x, g x)"