src/HOLCF/Ssum.thy
 changeset 19440 b2877e230b07 parent 18078 20e5a6440790 child 25131 2c8caac48ade
```--- a/src/HOLCF/Ssum.thy	Thu Apr 13 23:14:18 2006 +0200
+++ b/src/HOLCF/Ssum.thy	Thu Apr 13 23:15:44 2006 +0200
@@ -118,16 +118,16 @@
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 eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)

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 eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr)

lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
-by (simp add: po_eq_conv)
+by (subst po_eq_conv, simp)

lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
-by (simp add: po_eq_conv)
+by (subst po_eq_conv, simp)

subsection {* Chains of strict sums *}
```