removed LICENCE note -- everything is subject to Isabelle licence as
authorwenzelm
Wed May 25 09:44:34 2005 +0200 (2005-05-25)
changeset 160704a83dd540b88
parent 16069 3f2a9f400168
child 16071 e0136cdef722
removed LICENCE note -- everything is subject to Isabelle licence as
stated in COPYRIGHT file;
src/HOLCF/Adm.thy
src/HOLCF/Cfun.thy
src/HOLCF/Cont.thy
src/HOLCF/Cprod.thy
src/HOLCF/Discrete.thy
src/HOLCF/Domain.thy
src/HOLCF/Fix.thy
src/HOLCF/FunCpo.thy
src/HOLCF/One.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tr.thy
src/HOLCF/TypedefPcpo.thy
src/HOLCF/Up.thy
src/HOLCF/domain/extender.ML
     1.1 --- a/src/HOLCF/Adm.thy	Wed May 25 09:04:24 2005 +0200
     1.2 +++ b/src/HOLCF/Adm.thy	Wed May 25 09:44:34 2005 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      HOLCF/Adm.thy
     1.5      ID:         $Id$
     1.6      Author:     Franz Regensburger
     1.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  *)
     1.9  
    1.10  header {* Admissibility *}
     2.1 --- a/src/HOLCF/Cfun.thy	Wed May 25 09:04:24 2005 +0200
     2.2 +++ b/src/HOLCF/Cfun.thy	Wed May 25 09:44:34 2005 +0200
     2.3 @@ -1,10 +1,8 @@
     2.4  (*  Title:      HOLCF/Cfun.thy
     2.5      ID:         $Id$
     2.6      Author:     Franz Regensburger
     2.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  
     2.9  Definition of the type ->  of continuous functions.
    2.10 -
    2.11  *)
    2.12  
    2.13  header {* The type of continuous functions *}
     3.1 --- a/src/HOLCF/Cont.thy	Wed May 25 09:04:24 2005 +0200
     3.2 +++ b/src/HOLCF/Cont.thy	Wed May 25 09:44:34 2005 +0200
     3.3 @@ -1,9 +1,8 @@
     3.4  (*  Title:      HOLCF/Cont.thy
     3.5      ID:         $Id$
     3.6      Author:     Franz Regensburger
     3.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.8  
     3.9 -    Results about continuity and monotonicity
    3.10 +Results about continuity and monotonicity.
    3.11  *)
    3.12  
    3.13  header {* Continuity and monotonicity *}
     4.1 --- a/src/HOLCF/Cprod.thy	Wed May 25 09:04:24 2005 +0200
     4.2 +++ b/src/HOLCF/Cprod.thy	Wed May 25 09:44:34 2005 +0200
     4.3 @@ -1,9 +1,8 @@
     4.4  (*  Title:      HOLCF/Cprod.thy
     4.5      ID:         $Id$
     4.6      Author:     Franz Regensburger
     4.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.8  
     4.9 -Partial ordering for cartesian product of HOL theory prod.thy
    4.10 +Partial ordering for cartesian product of HOL products.
    4.11  *)
    4.12  
    4.13  header {* The cpo of cartesian products *}
     5.1 --- a/src/HOLCF/Discrete.thy	Wed May 25 09:04:24 2005 +0200
     5.2 +++ b/src/HOLCF/Discrete.thy	Wed May 25 09:44:34 2005 +0200
     5.3 @@ -1,7 +1,6 @@
     5.4  (*  Title:      HOLCF/Discrete.thy
     5.5      ID:         $Id$
     5.6      Author:     Tobias Nipkow
     5.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.8  
     5.9  Discrete CPOs.
    5.10  *)
     6.1 --- a/src/HOLCF/Domain.thy	Wed May 25 09:04:24 2005 +0200
     6.2 +++ b/src/HOLCF/Domain.thy	Wed May 25 09:44:34 2005 +0200
     6.3 @@ -1,7 +1,6 @@
     6.4  (*  Title:      HOLCF/Domain.thy
     6.5      ID:         $Id$
     6.6      Author:     Brian Huffman
     6.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.8  *)
     6.9  
    6.10  header {* Domain package *}
     7.1 --- a/src/HOLCF/Fix.thy	Wed May 25 09:04:24 2005 +0200
     7.2 +++ b/src/HOLCF/Fix.thy	Wed May 25 09:44:34 2005 +0200
     7.3 @@ -1,9 +1,8 @@
     7.4  (*  Title:      HOLCF/Fix.thy
     7.5      ID:         $Id$
     7.6      Author:     Franz Regensburger
     7.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.8  
     7.9 -definitions for fixed point operator and admissibility
    7.10 +Definitions for fixed point operator and admissibility.
    7.11  *)
    7.12  
    7.13  header {* Fixed point operator and admissibility *}
     8.1 --- a/src/HOLCF/FunCpo.thy	Wed May 25 09:04:24 2005 +0200
     8.2 +++ b/src/HOLCF/FunCpo.thy	Wed May 25 09:44:34 2005 +0200
     8.3 @@ -1,13 +1,12 @@
     8.4  (*  Title:      HOLCF/FunCpo.thy
     8.5      ID:         $Id$
     8.6      Author:     Franz Regensburger
     8.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.8  
     8.9  Definition of the partial ordering for the type of all functions => (fun)
    8.10  
    8.11  REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !!
    8.12  
    8.13 -Class instance of  => (fun) for class pcpo
    8.14 +Class instance of  => (fun) for class pcpo.
    8.15  *)
    8.16  
    8.17  header {* Class instances for the type of all functions *}
     9.1 --- a/src/HOLCF/One.thy	Wed May 25 09:04:24 2005 +0200
     9.2 +++ b/src/HOLCF/One.thy	Wed May 25 09:44:34 2005 +0200
     9.3 @@ -1,7 +1,8 @@
     9.4  (*  Title:      HOLCF/One.thy
     9.5      ID:         $Id$
     9.6      Author:     Oscar Slotosch
     9.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     9.8 +
     9.9 +The unit domain.
    9.10  *)
    9.11  
    9.12  header {* The unit domain *}
    9.13 @@ -19,14 +20,6 @@
    9.14  translations
    9.15    "one" <= (type) "unit lift" 
    9.16  
    9.17 -(*  Title:      HOLCF/One.ML
    9.18 -    ID:         $Id$
    9.19 -    Author:     Oscar Slotosch
    9.20 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    9.21 -
    9.22 -The unit domain.
    9.23 -*)
    9.24 -
    9.25  (* ------------------------------------------------------------------------ *)
    9.26  (* Exhaustion and Elimination for type one                                  *)
    9.27  (* ------------------------------------------------------------------------ *)
    10.1 --- a/src/HOLCF/Pcpo.thy	Wed May 25 09:04:24 2005 +0200
    10.2 +++ b/src/HOLCF/Pcpo.thy	Wed May 25 09:44:34 2005 +0200
    10.3 @@ -1,9 +1,8 @@
    10.4  (*  Title:      HOLCF/Pcpo.thy
    10.5      ID:         $Id$
    10.6      Author:     Franz Regensburger
    10.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    10.8  
    10.9 -introduction of the classes cpo and pcpo 
   10.10 +Introduction of the classes cpo and pcpo.
   10.11  *)
   10.12  
   10.13  header {* Classes cpo and pcpo *}
    11.1 --- a/src/HOLCF/Porder.thy	Wed May 25 09:04:24 2005 +0200
    11.2 +++ b/src/HOLCF/Porder.thy	Wed May 25 09:44:34 2005 +0200
    11.3 @@ -1,10 +1,9 @@
    11.4  (*  Title:      HOLCF/Porder.thy
    11.5      ID:         $Id$
    11.6      Author:     Franz Regensburger
    11.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    11.8  
    11.9  Definition of class porder (partial order).
   11.10 -Conservative extension of theory Porder0 by constant definitions 
   11.11 +Conservative extension of theory Porder0 by constant definitions.
   11.12  *)
   11.13  
   11.14  header {* Partial orders *}
    12.1 --- a/src/HOLCF/Sprod.thy	Wed May 25 09:04:24 2005 +0200
    12.2 +++ b/src/HOLCF/Sprod.thy	Wed May 25 09:44:34 2005 +0200
    12.3 @@ -1,7 +1,6 @@
    12.4  (*  Title:      HOLCF/Sprod.thy
    12.5      ID:         $Id$
    12.6      Author:     Franz Regensburger and Brian Huffman
    12.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    12.8  
    12.9  Strict product with typedef.
   12.10  *)
    13.1 --- a/src/HOLCF/Ssum.thy	Wed May 25 09:04:24 2005 +0200
    13.2 +++ b/src/HOLCF/Ssum.thy	Wed May 25 09:44:34 2005 +0200
    13.3 @@ -1,9 +1,8 @@
    13.4  (*  Title:      HOLCF/Ssum.thy
    13.5      ID:         $Id$
    13.6      Author:     Franz Regensburger and Brian Huffman
    13.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    13.8  
    13.9 -Strict sum with typedef
   13.10 +Strict sum with typedef.
   13.11  *)
   13.12  
   13.13  header {* The type of strict sums *}
    14.1 --- a/src/HOLCF/Tr.thy	Wed May 25 09:04:24 2005 +0200
    14.2 +++ b/src/HOLCF/Tr.thy	Wed May 25 09:44:34 2005 +0200
    14.3 @@ -1,9 +1,8 @@
    14.4  (*  Title:      HOLCF/Tr.thy
    14.5      ID:         $Id$
    14.6      Author:     Franz Regensburger
    14.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    14.8  
    14.9 -Introduce infix if_then_else_fi and boolean connectives andalso, orelse
   14.10 +Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
   14.11  *)
   14.12  
   14.13  header {* The type of lifted booleans *}
    15.1 --- a/src/HOLCF/TypedefPcpo.thy	Wed May 25 09:04:24 2005 +0200
    15.2 +++ b/src/HOLCF/TypedefPcpo.thy	Wed May 25 09:44:34 2005 +0200
    15.3 @@ -1,7 +1,6 @@
    15.4  (*  Title:      HOLCF/TypedefPcpo.thy
    15.5      ID:         $Id$
    15.6      Author:     Brian Huffman
    15.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    15.8  *)
    15.9  
   15.10  header {* Subtypes of pcpos *}
    16.1 --- a/src/HOLCF/Up.thy	Wed May 25 09:04:24 2005 +0200
    16.2 +++ b/src/HOLCF/Up.thy	Wed May 25 09:44:34 2005 +0200
    16.3 @@ -1,8 +1,6 @@
    16.4  (*  Title:      HOLCF/Up.thy
    16.5      ID:         $Id$
    16.6 -    Author:     Franz Regensburger
    16.7 -                Additions by Brian Huffman
    16.8 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    16.9 +    Author:     Franz Regensburger and Brian Huffman
   16.10  
   16.11  Lifting.
   16.12  *)
    17.1 --- a/src/HOLCF/domain/extender.ML	Wed May 25 09:04:24 2005 +0200
    17.2 +++ b/src/HOLCF/domain/extender.ML	Wed May 25 09:44:34 2005 +0200
    17.3 @@ -1,7 +1,6 @@
    17.4  (*  Title:      HOLCF/domain/extender.ML
    17.5      ID:         $Id$
    17.6      Author:     David von Oheimb
    17.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    17.8  
    17.9  Theory extender for domain section, including new-style theory syntax.
   17.10