remove cvs Id tags

--- a/src/HOLCF/Adm.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Adm.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Adm.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
 *)
 

--- a/src/HOLCF/Algebraic.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Algebraic.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Algebraic.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Bifinite.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Bifinite.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Bifinite.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Cfun.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Cfun.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Cfun.thy
-    ID:         $Id$
     Author:     Franz Regensburger
 
 Definition of the type ->  of continuous functions.

--- a/src/HOLCF/CompactBasis.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/CompactBasis.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/CompactBasis.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Completion.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Completion.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Completion.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Cont.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Cont.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Cont.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Results about continuity and monotonicity.
 *)
 
 header {* Continuity and monotonicity *}

--- a/src/HOLCF/ConvexPD.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/ConvexPD.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/ConvexPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Cprod.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Cprod.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Cprod.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Partial ordering for cartesian product of HOL products.
 *)
 
 header {* The cpo of cartesian products *}

--- a/src/HOLCF/Deflation.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Deflation.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Deflation.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Discrete.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Discrete.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Discrete.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
-
-Discrete CPOs.
 *)
 
 header {* Discrete cpo types *}

--- a/src/HOLCF/Domain.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Domain.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Domain.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Ffun.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Ffun.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,10 +1,5 @@
 (*  Title:      HOLCF/FunCpo.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Definition of the partial ordering for the type of all functions => (fun)
-
-Class instance of  => (fun) for class pcpo.
 *)
 
 header {* Class instances for the full function space *}

--- a/src/HOLCF/Fix.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Fix.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Fix.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Definitions for fixed point operator and admissibility.
 *)
 
 header {* Fixed point operator and admissibility *}

--- a/src/HOLCF/Fixrec.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Fixrec.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Fixrec.thy
-    ID:         $Id$
     Author:     Amber Telfer and Brian Huffman
 *)
 

--- a/src/HOLCF/HOLCF.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/HOLCF.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/HOLCF.thy
-    ID:         $Id$
     Author:     Franz Regensburger
 
 HOLCF -- a semantic extension of HOL by the LCF logic.

--- a/src/HOLCF/Lift.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Lift.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Lift.thy
-    ID:         $Id$
     Author:     Olaf Mueller
 *)
 

--- a/src/HOLCF/LowerPD.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/LowerPD.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/LowerPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/One.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/One.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/One.thy
-    ID:         $Id$
     Author:     Oscar Slotosch
-
-The unit domain.
 *)
 
 header {* The unit domain *}

--- a/src/HOLCF/Pcpo.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Pcpo.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Pcpo.thy
-    ID:         $Id$
     Author:     Franz Regensburger
 *)
 

--- a/src/HOLCF/Pcpodef.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Pcpodef.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Pcpodef.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Porder.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Porder.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Porder.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
 *)
 

--- a/src/HOLCF/Sprod.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Sprod.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Sprod.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-
-Strict product with typedef.
 *)
 
 header {* The type of strict products *}

--- a/src/HOLCF/Ssum.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Ssum.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Ssum.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-
-Strict sum with typedef.
 *)
 
 header {* The type of strict sums *}

--- a/src/HOLCF/Tr.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Tr.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Tr.thy
-    ID:         $Id$
     Author:     Franz Regensburger
-
-Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
 *)
 
 header {* The type of lifted booleans *}

--- a/src/HOLCF/Universal.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Universal.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Universal.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 

--- a/src/HOLCF/Up.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/Up.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,8 +1,5 @@
 (*  Title:      HOLCF/Up.thy
-    ID:         $Id$
     Author:     Franz Regensburger and Brian Huffman
-
-Lifting.
 *)
 
 header {* The type of lifted values *}

--- a/src/HOLCF/UpperPD.thy	Tue Dec 16 21:18:53 2008 -0800
+++ b/src/HOLCF/UpperPD.thy	Tue Dec 16 21:31:55 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/UpperPD.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)