fix headers
authorhuffman
Fri Mar 04 23:23:47 2005 +0100 (2005-03-04)
changeset 15577e16da3068ad6
parent 15576 efb95d0d01f7
child 15578 d364491ba718
fix headers
src/HOLCF/Cfun.thy
src/HOLCF/Cont.thy
src/HOLCF/Cprod.thy
src/HOLCF/Fix.thy
src/HOLCF/FunCpo.thy
src/HOLCF/Lift.thy
src/HOLCF/One.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Fri Mar 04 23:12:36 2005 +0100
     1.2 +++ b/src/HOLCF/Cfun.thy	Fri Mar 04 23:23:47 2005 +0100
     1.3 @@ -9,7 +9,9 @@
     1.4  
     1.5  header {* The type of continuous functions *}
     1.6  
     1.7 -theory Cfun = Cont:
     1.8 +theory Cfun
     1.9 +imports Cont
    1.10 +begin
    1.11  
    1.12  defaultsort cpo
    1.13  
     2.1 --- a/src/HOLCF/Cont.thy	Fri Mar 04 23:12:36 2005 +0100
     2.2 +++ b/src/HOLCF/Cont.thy	Fri Mar 04 23:23:47 2005 +0100
     2.3 @@ -6,7 +6,11 @@
     2.4      Results about continuity and monotonicity
     2.5  *)
     2.6  
     2.7 -theory Cont = FunCpo:
     2.8 +header {* Continuity and monotonicity *}
     2.9 +
    2.10 +theory Cont
    2.11 +imports FunCpo
    2.12 +begin
    2.13  
    2.14  (* 
    2.15  
     3.1 --- a/src/HOLCF/Cprod.thy	Fri Mar 04 23:12:36 2005 +0100
     3.2 +++ b/src/HOLCF/Cprod.thy	Fri Mar 04 23:23:47 2005 +0100
     3.3 @@ -8,7 +8,9 @@
     3.4  
     3.5  header {* The cpo of cartesian products *}
     3.6  
     3.7 -theory Cprod = Cfun:
     3.8 +theory Cprod
     3.9 +imports Cfun
    3.10 +begin
    3.11  
    3.12  defaultsort cpo
    3.13  
    3.14 @@ -231,7 +233,7 @@
    3.15    "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
    3.16  
    3.17  syntax (xsymbols)
    3.18 -  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
    3.19 +  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
    3.20  
    3.21  (* for compatibility with old HOLCF-Version *)
    3.22  lemma inst_cprod_pcpo: "UU = (UU,UU)"
     4.1 --- a/src/HOLCF/Fix.thy	Fri Mar 04 23:12:36 2005 +0100
     4.2 +++ b/src/HOLCF/Fix.thy	Fri Mar 04 23:23:47 2005 +0100
     4.3 @@ -6,7 +6,11 @@
     4.4  definitions for fixed point operator and admissibility
     4.5  *)
     4.6  
     4.7 -theory Fix = Cfun:
     4.8 +header {* Fixed point operator and admissibility *}
     4.9 +
    4.10 +theory Fix
    4.11 +imports Cfun
    4.12 +begin
    4.13  
    4.14  consts
    4.15  
     5.1 --- a/src/HOLCF/FunCpo.thy	Fri Mar 04 23:12:36 2005 +0100
     5.2 +++ b/src/HOLCF/FunCpo.thy	Fri Mar 04 23:23:47 2005 +0100
     5.3 @@ -12,7 +12,9 @@
     5.4  
     5.5  header {* Class instances for the type of all functions *}
     5.6  
     5.7 -theory FunCpo = Pcpo:
     5.8 +theory FunCpo
     5.9 +imports Pcpo
    5.10 +begin
    5.11  
    5.12  (* to make << defineable: *)
    5.13  
     6.1 --- a/src/HOLCF/Lift.thy	Fri Mar 04 23:12:36 2005 +0100
     6.2 +++ b/src/HOLCF/Lift.thy	Fri Mar 04 23:23:47 2005 +0100
     6.3 @@ -5,7 +5,9 @@
     6.4  
     6.5  header {* Lifting types of class type to flat pcpo's *}
     6.6  
     6.7 -theory Lift = Cprod:
     6.8 +theory Lift
     6.9 +imports Cprod
    6.10 +begin
    6.11  
    6.12  defaultsort type
    6.13  
     7.1 --- a/src/HOLCF/One.thy	Fri Mar 04 23:12:36 2005 +0100
     7.2 +++ b/src/HOLCF/One.thy	Fri Mar 04 23:23:47 2005 +0100
     7.3 @@ -4,7 +4,11 @@
     7.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.5  *)
     7.6  
     7.7 -theory One = Lift:
     7.8 +header {* The unit domain *}
     7.9 +
    7.10 +theory One
    7.11 +imports Lift
    7.12 +begin
    7.13  
    7.14  types one = "unit lift"
    7.15  
     8.1 --- a/src/HOLCF/Pcpo.thy	Fri Mar 04 23:12:36 2005 +0100
     8.2 +++ b/src/HOLCF/Pcpo.thy	Fri Mar 04 23:23:47 2005 +0100
     8.3 @@ -8,7 +8,9 @@
     8.4  
     8.5  header {* Classes cpo and pcpo *}
     8.6  
     8.7 -theory Pcpo = Porder:
     8.8 +theory Pcpo
     8.9 +imports Porder
    8.10 +begin
    8.11  
    8.12  (* The class cpo of chain complete partial orders *)
    8.13  (* ********************************************** *)
     9.1 --- a/src/HOLCF/Porder.thy	Fri Mar 04 23:12:36 2005 +0100
     9.2 +++ b/src/HOLCF/Porder.thy	Fri Mar 04 23:23:47 2005 +0100
     9.3 @@ -9,7 +9,9 @@
     9.4  
     9.5  header {* Type class of partial orders *}
     9.6  
     9.7 -theory Porder = Main:
     9.8 +theory Porder
     9.9 +imports Main
    9.10 +begin
    9.11  
    9.12  	(* introduce a (syntactic) class for the constant << *)
    9.13  axclass sq_ord < type
    10.1 --- a/src/HOLCF/Sprod.thy	Fri Mar 04 23:12:36 2005 +0100
    10.2 +++ b/src/HOLCF/Sprod.thy	Fri Mar 04 23:23:47 2005 +0100
    10.3 @@ -8,7 +8,9 @@
    10.4  
    10.5  header {* The type of strict products *}
    10.6  
    10.7 -theory Sprod = Cfun:
    10.8 +theory Sprod
    10.9 +imports Cfun
   10.10 +begin
   10.11  
   10.12  constdefs
   10.13    Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
    11.1 --- a/src/HOLCF/Ssum.thy	Fri Mar 04 23:12:36 2005 +0100
    11.2 +++ b/src/HOLCF/Ssum.thy	Fri Mar 04 23:23:47 2005 +0100
    11.3 @@ -8,7 +8,9 @@
    11.4  
    11.5  header {* The type of strict sums *}
    11.6  
    11.7 -theory Ssum = Cfun:
    11.8 +theory Ssum
    11.9 +imports Cfun
   11.10 +begin
   11.11  
   11.12  constdefs
   11.13    Sinl_Rep      :: "['a,'a,'b,bool]=>bool"
    12.1 --- a/src/HOLCF/Up.thy	Fri Mar 04 23:12:36 2005 +0100
    12.2 +++ b/src/HOLCF/Up.thy	Fri Mar 04 23:23:47 2005 +0100
    12.3 @@ -8,7 +8,9 @@
    12.4  
    12.5  header {* The type of lifted values *}
    12.6  
    12.7 -theory Up = Cfun + Sum_Type + Datatype:
    12.8 +theory Up
    12.9 +imports Cfun Sum_Type Datatype
   12.10 +begin
   12.11  
   12.12  (* new type for lifting *)
   12.13