--- a/src/HOLCF/Cprod.thy Tue Oct 11 23:47:29 2005 +0200
+++ b/src/HOLCF/Cprod.thy Wed Oct 12 01:43:37 2005 +0200
@@ -274,6 +274,9 @@
lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
by (auto simp add: po_eq_conv less_cprod)
+lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
+by (rule compactI, simp add: less_cprod)
+
lemma lub_cprod2:
"chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)