remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2

--- a/src/HOLCF/Cfun.thy	Mon Oct 11 21:35:31 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Tue Oct 12 05:25:21 2010 -0700
@@ -600,10 +600,10 @@
 using f
 proof (rule cont2cont_Let)
   fix x show "cont (\<lambda>y. g x y)"
-    using g by (rule cont_fst_snd_D2)
+    using g by (simp add: prod_cont_iff)
 next
   fix y show "cont (\<lambda>x. g x y)"
-    using g by (rule cont_fst_snd_D1)
+    using g by (simp add: prod_cont_iff)
 qed
 
 text {* The simple version (suggested by Joachim Breitner) is needed if

--- a/src/HOLCF/Product_Cpo.thy	Mon Oct 11 21:35:31 2010 -0700
+++ b/src/HOLCF/Product_Cpo.thy	Tue Oct 12 05:25:21 2010 -0700
@@ -267,14 +267,6 @@
 apply (simp only: prod_contI)
 done
 
-lemma cont_fst_snd_D1:
-  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>x. f x y)"
-by (drule cont_compose [OF _ cont_pair1], simp)
-
-lemma cont_fst_snd_D2:
-  "cont (\<lambda>p. f (fst p) (snd p)) \<Longrightarrow> cont (\<lambda>y. f x y)"
-by (drule cont_compose [OF _ cont_pair2], simp)
-
 lemma cont2cont_prod_case' [simp, cont2cont]:
   assumes f: "cont (\<lambda>p. f (fst p) (fst (snd p)) (snd (snd p)))"
   assumes g: "cont (\<lambda>x. g x)"