# HG changeset patch
# User huffman
# Date 1286886321 25200
# Node ID 427106657e044712433dd2cc3f5a172f5b17e7e3
# Parent  c5b5f7a3a3b13bb8de23ee75416608ac0c0bda9e
remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2

diff -r c5b5f7a3a3b1 -r 427106657e04 src/HOLCF/Cfun.thy
--- 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
diff -r c5b5f7a3a3b1 -r 427106657e04 src/HOLCF/Product_Cpo.thy
--- 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)"