diff -r f432973ce0f6 -r 84edf7177d73 src/HOLCF/Product_Cpo.thy
--- a/src/HOLCF/Product_Cpo.thy	Wed Nov 17 08:47:58 2010 -0800
+++ b/src/HOLCF/Product_Cpo.thy	Wed Nov 17 11:07:02 2010 -0800
@@ -276,6 +276,13 @@
  shows "cont (\<lambda>x. case p of (a, b) \<Rightarrow> f x a b)"
 using assms by (cases p) auto
 
+text {* Admissibility of predicates on product types. *}
+
+lemma adm_prod_case [simp]:
+  assumes "adm (\<lambda>x. P x (fst (f x)) (snd (f x)))"
+  shows "adm (\<lambda>x. case f x of (a, b) \<Rightarrow> P x a b)"
+unfolding prod_case_beta using assms .
+
 subsection {* Compactness and chain-finiteness *}
 
 lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"