--- a/src/HOLCF/Ssum.thy Wed Jul 13 20:53:26 2005 +0200
+++ b/src/HOLCF/Ssum.thy Thu Jul 14 01:04:30 2005 +0200
@@ -206,13 +206,9 @@
apply (rule contI)
apply (drule ssum_chain_lemma, safe)
apply (simp add: contlub_cfun_arg [symmetric])
-apply (simp add: Iwhen4)
-apply (simp add: contlub_cfun_arg)
-apply (simp add: thelubE chain_monofun)
+apply (simp add: Iwhen4 cont_cfun_arg)
apply (simp add: contlub_cfun_arg [symmetric])
-apply (simp add: Iwhen5)
-apply (simp add: contlub_cfun_arg)
-apply (simp add: thelubE chain_monofun)
+apply (simp add: Iwhen5 cont_cfun_arg)
done
subsection {* Continuous versions of constants *}