# HG changeset patch
# User huffman
# Date 1109975027 -3600
# Node ID e16da3068ad649222051b7e2790b495eb5d39b01
# Parent  efb95d0d01f7258047b067cbf176f17d3260ba06
fix headers

diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Cfun.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -9,7 +9,9 @@
 
 header {* The type of continuous functions *}
 
-theory Cfun = Cont:
+theory Cfun
+imports Cont
+begin
 
 defaultsort cpo
 
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Cont.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -6,7 +6,11 @@
     Results about continuity and monotonicity
 *)
 
-theory Cont = FunCpo:
+header {* Continuity and monotonicity *}
+
+theory Cont
+imports FunCpo
+begin
 
 (* 
 
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Cprod.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -8,7 +8,9 @@
 
 header {* The cpo of cartesian products *}
 
-theory Cprod = Cfun:
+theory Cprod
+imports Cfun
+begin
 
 defaultsort cpo
 
@@ -231,7 +233,7 @@
   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
 
 syntax (xsymbols)
-  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
+  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
 
 (* for compatibility with old HOLCF-Version *)
 lemma inst_cprod_pcpo: "UU = (UU,UU)"
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Fix.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -6,7 +6,11 @@
 definitions for fixed point operator and admissibility
 *)
 
-theory Fix = Cfun:
+header {* Fixed point operator and admissibility *}
+
+theory Fix
+imports Cfun
+begin
 
 consts
 
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/FunCpo.thy
--- a/src/HOLCF/FunCpo.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/FunCpo.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -12,7 +12,9 @@
 
 header {* Class instances for the type of all functions *}
 
-theory FunCpo = Pcpo:
+theory FunCpo
+imports Pcpo
+begin
 
 (* to make << defineable: *)
 
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Lift.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -5,7 +5,9 @@
 
 header {* Lifting types of class type to flat pcpo's *}
 
-theory Lift = Cprod:
+theory Lift
+imports Cprod
+begin
 
 defaultsort type
 
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/One.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -4,7 +4,11 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-theory One = Lift:
+header {* The unit domain *}
+
+theory One
+imports Lift
+begin
 
 types one = "unit lift"
 
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Pcpo.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -8,7 +8,9 @@
 
 header {* Classes cpo and pcpo *}
 
-theory Pcpo = Porder:
+theory Pcpo
+imports Porder
+begin
 
 (* The class cpo of chain complete partial orders *)
 (* ********************************************** *)
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Porder.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -9,7 +9,9 @@
 
 header {* Type class of partial orders *}
 
-theory Porder = Main:
+theory Porder
+imports Main
+begin
 
 	(* introduce a (syntactic) class for the constant << *)
 axclass sq_ord < type
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Sprod.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -8,7 +8,9 @@
 
 header {* The type of strict products *}
 
-theory Sprod = Cfun:
+theory Sprod
+imports Cfun
+begin
 
 constdefs
   Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Ssum.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -8,7 +8,9 @@
 
 header {* The type of strict sums *}
 
-theory Ssum = Cfun:
+theory Ssum
+imports Cfun
+begin
 
 constdefs
   Sinl_Rep      :: "['a,'a,'b,bool]=>bool"
diff -r efb95d0d01f7 -r e16da3068ad6 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/Up.thy	Fri Mar 04 23:23:47 2005 +0100
@@ -8,7 +8,9 @@
 
 header {* The type of lifted values *}
 
-theory Up = Cfun + Sum_Type + Datatype:
+theory Up
+imports Cfun Sum_Type Datatype
+begin
 
 (* new type for lifting *)