--- a/src/HOLCF/Ssum.thy Thu Nov 03 01:02:29 2005 +0100
+++ b/src/HOLCF/Ssum.thy Thu Nov 03 01:11:39 2005 +0100
@@ -112,16 +112,16 @@
subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
+by (simp add: less_Ssum_def Rep_Ssum_sinl)
lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
+by (simp add: less_Ssum_def Rep_Ssum_sinr)
lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr eq_UU_iff)
lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
by (simp add: po_eq_conv)
@@ -218,7 +218,11 @@
"sscase \<equiv> \<Lambda> f g s. Iwhen f g s"
translations
-"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s"
+ "case s of sinl\<cdot>x \<Rightarrow> t1 | sinr\<cdot>y \<Rightarrow> t2" == "sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+
+translations
+ "\<Lambda>(sinl\<cdot>x). t" == "sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
+ "\<Lambda>(sinr\<cdot>y). t" == "sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
text {* continuous versions of lemmas for @{term sscase} *}