--- 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
--- 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
(*
--- 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)"
--- 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
--- 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: *)
--- 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
--- 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"
--- 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 *)
(* ********************************************** *)
--- 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
--- 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"
--- 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"
--- 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 *)