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 *}