--- a/src/HOL/UNITY/Comp/Counter.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy Sat Oct 17 14:43:18 2009 +0200
@@ -1,12 +1,11 @@
-(* Title: HOL/UNITY/Counter
- ID: $Id$
+(* Title: HOL/UNITY/Comp/Counter.thy
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
From Charpentier and Chandy,
Examples of Program Composition Illustrating the Use of Universal Properties
In J. Rolim (editor), Parallel and Distributed Processing,
- Spriner LNCS 1586 (1999), pages 1215-1227.
+ Springer LNCS 1586 (1999), pages 1215-1227.
*)
header{*A Family of Similar Counters: Original Version*}
@@ -38,7 +37,7 @@
Component :: "nat => state program"
"Component i ==
mk_total_program({s. s C = 0 & s (c i) = 0}, {a i},
- \<Union>G \<in> preserves (%s. s (c i)). Acts G)"
+ \<Union>G \<in> preserves (%s. s (c i)). Acts G)"