--- 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)"