# HG changeset patch
# User huffman
# Date 1231985928 28800
# Node ID 7f4a32134447daa6706f8e819b569b9beab07f37
# Parent  59bee7985149aad5e55df04c968e74fef7b24449
minimize dependencies

diff -r 59bee7985149 -r 7f4a32134447 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Jan 14 18:05:05 2009 -0800
+++ b/src/HOLCF/Cfun.thy	Wed Jan 14 18:18:48 2009 -0800
@@ -7,7 +7,7 @@
 header {* The type of continuous functions *}
 
 theory Cfun
-imports Pcpodef Product_Cpo
+imports Pcpodef Ffun Product_Cpo
 begin
 
 defaultsort cpo
diff -r 59bee7985149 -r 7f4a32134447 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Wed Jan 14 18:05:05 2009 -0800
+++ b/src/HOLCF/Product_Cpo.thy	Wed Jan 14 18:18:48 2009 -0800
@@ -5,7 +5,7 @@
 header {* The cpo of cartesian products *}
 
 theory Product_Cpo
-imports Ffun
+imports Cont
 begin
 
 defaultsort cpo
@@ -192,12 +192,13 @@
   assumes f: "cont (\<lambda>x. f x)"
   assumes g: "cont (\<lambda>x. g x)"
   shows "cont (\<lambda>x. (f x, g x))"
-apply (rule cont2cont_app2 [OF cont2cont_lambda cont_pair2 g])
-apply (rule cont2cont_app2 [OF cont_const cont_pair1 f])
+apply (rule cont2cont_apply [OF _ cont_pair1 f])
+apply (rule cont2cont_apply [OF _ cont_pair2 g])
+apply (rule cont_const)
 done
 
-lemmas cont2cont_fst [cont2cont] = cont2cont_app3 [OF cont_fst]
+lemmas cont2cont_fst [cont2cont] = cont2cont_compose [OF cont_fst]
 
-lemmas cont2cont_snd [cont2cont] = cont2cont_app3 [OF cont_snd]
+lemmas cont2cont_snd [cont2cont] = cont2cont_compose [OF cont_snd]
 
 end