remove cvs Id tags
authorhuffman
Tue Dec 16 21:31:55 2008 -0800 (2008-12-16)
changeset 29138661a8db7e647
parent 29131 fd8bb7527f7b
child 29139 6e0b7b114072
remove cvs Id tags
src/HOLCF/Adm.thy
src/HOLCF/Algebraic.thy
src/HOLCF/Bifinite.thy
src/HOLCF/Cfun.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/Completion.thy
src/HOLCF/Cont.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Cprod.thy
src/HOLCF/Deflation.thy
src/HOLCF/Discrete.thy
src/HOLCF/Domain.thy
src/HOLCF/Ffun.thy
src/HOLCF/Fix.thy
src/HOLCF/Fixrec.thy
src/HOLCF/HOLCF.thy
src/HOLCF/Lift.thy
src/HOLCF/LowerPD.thy
src/HOLCF/One.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Porder.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tr.thy
src/HOLCF/Universal.thy
src/HOLCF/Up.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Adm.thy	Tue Dec 16 21:18:53 2008 -0800
     1.2 +++ b/src/HOLCF/Adm.thy	Tue Dec 16 21:31:55 2008 -0800
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOLCF/Adm.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Franz Regensburger and Brian Huffman
     1.7  *)
     1.8  
     2.1 --- a/src/HOLCF/Algebraic.thy	Tue Dec 16 21:18:53 2008 -0800
     2.2 +++ b/src/HOLCF/Algebraic.thy	Tue Dec 16 21:31:55 2008 -0800
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOLCF/Algebraic.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Brian Huffman
     2.7  *)
     2.8  
     3.1 --- a/src/HOLCF/Bifinite.thy	Tue Dec 16 21:18:53 2008 -0800
     3.2 +++ b/src/HOLCF/Bifinite.thy	Tue Dec 16 21:31:55 2008 -0800
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOLCF/Bifinite.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Brian Huffman
     3.7  *)
     3.8  
     4.1 --- a/src/HOLCF/Cfun.thy	Tue Dec 16 21:18:53 2008 -0800
     4.2 +++ b/src/HOLCF/Cfun.thy	Tue Dec 16 21:31:55 2008 -0800
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOLCF/Cfun.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Franz Regensburger
     4.7  
     4.8  Definition of the type ->  of continuous functions.
     5.1 --- a/src/HOLCF/CompactBasis.thy	Tue Dec 16 21:18:53 2008 -0800
     5.2 +++ b/src/HOLCF/CompactBasis.thy	Tue Dec 16 21:31:55 2008 -0800
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOLCF/CompactBasis.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Brian Huffman
     5.7  *)
     5.8  
     6.1 --- a/src/HOLCF/Completion.thy	Tue Dec 16 21:18:53 2008 -0800
     6.2 +++ b/src/HOLCF/Completion.thy	Tue Dec 16 21:31:55 2008 -0800
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOLCF/Completion.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Brian Huffman
     6.7  *)
     6.8  
     7.1 --- a/src/HOLCF/Cont.thy	Tue Dec 16 21:18:53 2008 -0800
     7.2 +++ b/src/HOLCF/Cont.thy	Tue Dec 16 21:31:55 2008 -0800
     7.3 @@ -1,8 +1,5 @@
     7.4  (*  Title:      HOLCF/Cont.thy
     7.5 -    ID:         $Id$
     7.6      Author:     Franz Regensburger
     7.7 -
     7.8 -Results about continuity and monotonicity.
     7.9  *)
    7.10  
    7.11  header {* Continuity and monotonicity *}
     8.1 --- a/src/HOLCF/ConvexPD.thy	Tue Dec 16 21:18:53 2008 -0800
     8.2 +++ b/src/HOLCF/ConvexPD.thy	Tue Dec 16 21:31:55 2008 -0800
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      HOLCF/ConvexPD.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Brian Huffman
     8.7  *)
     8.8  
     9.1 --- a/src/HOLCF/Cprod.thy	Tue Dec 16 21:18:53 2008 -0800
     9.2 +++ b/src/HOLCF/Cprod.thy	Tue Dec 16 21:31:55 2008 -0800
     9.3 @@ -1,8 +1,5 @@
     9.4  (*  Title:      HOLCF/Cprod.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Franz Regensburger
     9.7 -
     9.8 -Partial ordering for cartesian product of HOL products.
     9.9  *)
    9.10  
    9.11  header {* The cpo of cartesian products *}
    10.1 --- a/src/HOLCF/Deflation.thy	Tue Dec 16 21:18:53 2008 -0800
    10.2 +++ b/src/HOLCF/Deflation.thy	Tue Dec 16 21:31:55 2008 -0800
    10.3 @@ -1,5 +1,4 @@
    10.4  (*  Title:      HOLCF/Deflation.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Brian Huffman
    10.7  *)
    10.8  
    11.1 --- a/src/HOLCF/Discrete.thy	Tue Dec 16 21:18:53 2008 -0800
    11.2 +++ b/src/HOLCF/Discrete.thy	Tue Dec 16 21:31:55 2008 -0800
    11.3 @@ -1,8 +1,5 @@
    11.4  (*  Title:      HOLCF/Discrete.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Tobias Nipkow
    11.7 -
    11.8 -Discrete CPOs.
    11.9  *)
   11.10  
   11.11  header {* Discrete cpo types *}
    12.1 --- a/src/HOLCF/Domain.thy	Tue Dec 16 21:18:53 2008 -0800
    12.2 +++ b/src/HOLCF/Domain.thy	Tue Dec 16 21:31:55 2008 -0800
    12.3 @@ -1,5 +1,4 @@
    12.4  (*  Title:      HOLCF/Domain.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Brian Huffman
    12.7  *)
    12.8  
    13.1 --- a/src/HOLCF/Ffun.thy	Tue Dec 16 21:18:53 2008 -0800
    13.2 +++ b/src/HOLCF/Ffun.thy	Tue Dec 16 21:31:55 2008 -0800
    13.3 @@ -1,10 +1,5 @@
    13.4  (*  Title:      HOLCF/FunCpo.thy
    13.5 -    ID:         $Id$
    13.6      Author:     Franz Regensburger
    13.7 -
    13.8 -Definition of the partial ordering for the type of all functions => (fun)
    13.9 -
   13.10 -Class instance of  => (fun) for class pcpo.
   13.11  *)
   13.12  
   13.13  header {* Class instances for the full function space *}
    14.1 --- a/src/HOLCF/Fix.thy	Tue Dec 16 21:18:53 2008 -0800
    14.2 +++ b/src/HOLCF/Fix.thy	Tue Dec 16 21:31:55 2008 -0800
    14.3 @@ -1,8 +1,5 @@
    14.4  (*  Title:      HOLCF/Fix.thy
    14.5 -    ID:         $Id$
    14.6      Author:     Franz Regensburger
    14.7 -
    14.8 -Definitions for fixed point operator and admissibility.
    14.9  *)
   14.10  
   14.11  header {* Fixed point operator and admissibility *}
    15.1 --- a/src/HOLCF/Fixrec.thy	Tue Dec 16 21:18:53 2008 -0800
    15.2 +++ b/src/HOLCF/Fixrec.thy	Tue Dec 16 21:31:55 2008 -0800
    15.3 @@ -1,5 +1,4 @@
    15.4  (*  Title:      HOLCF/Fixrec.thy
    15.5 -    ID:         $Id$
    15.6      Author:     Amber Telfer and Brian Huffman
    15.7  *)
    15.8  
    16.1 --- a/src/HOLCF/HOLCF.thy	Tue Dec 16 21:18:53 2008 -0800
    16.2 +++ b/src/HOLCF/HOLCF.thy	Tue Dec 16 21:31:55 2008 -0800
    16.3 @@ -1,5 +1,4 @@
    16.4  (*  Title:      HOLCF/HOLCF.thy
    16.5 -    ID:         $Id$
    16.6      Author:     Franz Regensburger
    16.7  
    16.8  HOLCF -- a semantic extension of HOL by the LCF logic.
    17.1 --- a/src/HOLCF/Lift.thy	Tue Dec 16 21:18:53 2008 -0800
    17.2 +++ b/src/HOLCF/Lift.thy	Tue Dec 16 21:31:55 2008 -0800
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      HOLCF/Lift.thy
    17.5 -    ID:         $Id$
    17.6      Author:     Olaf Mueller
    17.7  *)
    17.8  
    18.1 --- a/src/HOLCF/LowerPD.thy	Tue Dec 16 21:18:53 2008 -0800
    18.2 +++ b/src/HOLCF/LowerPD.thy	Tue Dec 16 21:31:55 2008 -0800
    18.3 @@ -1,5 +1,4 @@
    18.4  (*  Title:      HOLCF/LowerPD.thy
    18.5 -    ID:         $Id$
    18.6      Author:     Brian Huffman
    18.7  *)
    18.8  
    19.1 --- a/src/HOLCF/One.thy	Tue Dec 16 21:18:53 2008 -0800
    19.2 +++ b/src/HOLCF/One.thy	Tue Dec 16 21:31:55 2008 -0800
    19.3 @@ -1,8 +1,5 @@
    19.4  (*  Title:      HOLCF/One.thy
    19.5 -    ID:         $Id$
    19.6      Author:     Oscar Slotosch
    19.7 -
    19.8 -The unit domain.
    19.9  *)
   19.10  
   19.11  header {* The unit domain *}
    20.1 --- a/src/HOLCF/Pcpo.thy	Tue Dec 16 21:18:53 2008 -0800
    20.2 +++ b/src/HOLCF/Pcpo.thy	Tue Dec 16 21:31:55 2008 -0800
    20.3 @@ -1,5 +1,4 @@
    20.4  (*  Title:      HOLCF/Pcpo.thy
    20.5 -    ID:         $Id$
    20.6      Author:     Franz Regensburger
    20.7  *)
    20.8  
    21.1 --- a/src/HOLCF/Pcpodef.thy	Tue Dec 16 21:18:53 2008 -0800
    21.2 +++ b/src/HOLCF/Pcpodef.thy	Tue Dec 16 21:31:55 2008 -0800
    21.3 @@ -1,5 +1,4 @@
    21.4  (*  Title:      HOLCF/Pcpodef.thy
    21.5 -    ID:         $Id$
    21.6      Author:     Brian Huffman
    21.7  *)
    21.8  
    22.1 --- a/src/HOLCF/Porder.thy	Tue Dec 16 21:18:53 2008 -0800
    22.2 +++ b/src/HOLCF/Porder.thy	Tue Dec 16 21:31:55 2008 -0800
    22.3 @@ -1,5 +1,4 @@
    22.4  (*  Title:      HOLCF/Porder.thy
    22.5 -    ID:         $Id$
    22.6      Author:     Franz Regensburger and Brian Huffman
    22.7  *)
    22.8  
    23.1 --- a/src/HOLCF/Sprod.thy	Tue Dec 16 21:18:53 2008 -0800
    23.2 +++ b/src/HOLCF/Sprod.thy	Tue Dec 16 21:31:55 2008 -0800
    23.3 @@ -1,8 +1,5 @@
    23.4  (*  Title:      HOLCF/Sprod.thy
    23.5 -    ID:         $Id$
    23.6      Author:     Franz Regensburger and Brian Huffman
    23.7 -
    23.8 -Strict product with typedef.
    23.9  *)
   23.10  
   23.11  header {* The type of strict products *}
    24.1 --- a/src/HOLCF/Ssum.thy	Tue Dec 16 21:18:53 2008 -0800
    24.2 +++ b/src/HOLCF/Ssum.thy	Tue Dec 16 21:31:55 2008 -0800
    24.3 @@ -1,8 +1,5 @@
    24.4  (*  Title:      HOLCF/Ssum.thy
    24.5 -    ID:         $Id$
    24.6      Author:     Franz Regensburger and Brian Huffman
    24.7 -
    24.8 -Strict sum with typedef.
    24.9  *)
   24.10  
   24.11  header {* The type of strict sums *}
    25.1 --- a/src/HOLCF/Tr.thy	Tue Dec 16 21:18:53 2008 -0800
    25.2 +++ b/src/HOLCF/Tr.thy	Tue Dec 16 21:31:55 2008 -0800
    25.3 @@ -1,8 +1,5 @@
    25.4  (*  Title:      HOLCF/Tr.thy
    25.5 -    ID:         $Id$
    25.6      Author:     Franz Regensburger
    25.7 -
    25.8 -Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
    25.9  *)
   25.10  
   25.11  header {* The type of lifted booleans *}
    26.1 --- a/src/HOLCF/Universal.thy	Tue Dec 16 21:18:53 2008 -0800
    26.2 +++ b/src/HOLCF/Universal.thy	Tue Dec 16 21:31:55 2008 -0800
    26.3 @@ -1,5 +1,4 @@
    26.4  (*  Title:      HOLCF/Universal.thy
    26.5 -    ID:         $Id$
    26.6      Author:     Brian Huffman
    26.7  *)
    26.8  
    27.1 --- a/src/HOLCF/Up.thy	Tue Dec 16 21:18:53 2008 -0800
    27.2 +++ b/src/HOLCF/Up.thy	Tue Dec 16 21:31:55 2008 -0800
    27.3 @@ -1,8 +1,5 @@
    27.4  (*  Title:      HOLCF/Up.thy
    27.5 -    ID:         $Id$
    27.6      Author:     Franz Regensburger and Brian Huffman
    27.7 -
    27.8 -Lifting.
    27.9  *)
   27.10  
   27.11  header {* The type of lifted values *}
    28.1 --- a/src/HOLCF/UpperPD.thy	Tue Dec 16 21:18:53 2008 -0800
    28.2 +++ b/src/HOLCF/UpperPD.thy	Tue Dec 16 21:31:55 2008 -0800
    28.3 @@ -1,5 +1,4 @@
    28.4  (*  Title:      HOLCF/UpperPD.thy
    28.5 -    ID:         $Id$
    28.6      Author:     Brian Huffman
    28.7  *)
    28.8