# HG changeset patch
# User huffman
# Date 1229491915 28800
# Node ID 661a8db7e647cae6a0241f5198bbb92256b40af4
# Parent  fd8bb7527f7bee017a79357614f582fe0e666e51
remove cvs Id tags

diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Adm.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Algebraic.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Bifinite.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Cfun.thy
--- 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.
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/CompactBasis.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Completion.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Cont.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/ConvexPD.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Cprod.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Deflation.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Discrete.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Domain.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Ffun.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Fix.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Fixrec.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/HOLCF.thy
--- 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.
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Lift.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/LowerPD.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/One.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Pcpo.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Pcpodef.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Porder.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Sprod.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Ssum.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Tr.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Universal.thy
--- 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
 *)
 
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/Up.thy
--- 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 *}
diff -r fd8bb7527f7b -r 661a8db7e647 src/HOLCF/UpperPD.thy
--- 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
 *)