diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -21,6 +21,12 @@
     (cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
 by simp
 
+instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
+by (rule typedef_finite_po [OF type_definition_Ssum])
+
+instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
+by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def])
+
 syntax (xsymbols)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 syntax (HTML output)
@@ -186,4 +192,18 @@
 lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
 by (cases z, simp_all)
 
+subsection {* Strict sum preserves flatness *}
+
+lemma flat_less_iff:
+  fixes x y :: "'a::flat"
+  shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
+by (safe dest!: ax_flat [rule_format])
+
+instance "++" :: (flat, flat) flat
+apply (intro_classes, clarify)
+apply (rule_tac p=x in ssumE, simp)
+apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
+apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
+done
+
 end