Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified proof of cont_Iwhen3
authorhuffman
Thu, 14 Jul 2005 01:04:30 +0200
changeset 16823 13f3768a6f14
parent 16822 7fa91e6176ed
child 16824 c889f499911c
simplified proof of cont_Iwhen3
src/HOLCF/Ssum.thy file | annotate | diff | comparison | revisions 
--- 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 *}
isabelle