# HG changeset patch
# User huffman
# Date 1121295870 -7200
# Node ID 13f3768a6f14bc4d6d47d111d4494f3a12289f61
# Parent  7fa91e6176ed2cb914474b376a74255b6886b082
simplified proof of cont_Iwhen3

diff -r 7fa91e6176ed -r 13f3768a6f14 src/HOLCF/Ssum.thy
--- 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 *}