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.
use theorem ch2ch_cont
authorhuffman
Thu, 07 Jul 2005 18:38:00 +0200
changeset 16742 d1641dba61e5
parent 16741 7a6c17b826c0
child 16743 21dbff595bf6
use theorem ch2ch_cont
src/HOLCF/Ssum.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Ssum.thy	Thu Jul 07 18:25:02 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Thu Jul 07 18:38:00 2005 +0200
@@ -148,7 +148,7 @@
   apply (rule_tac x="\<lambda>i. cfst\<cdot>(Rep_Ssum (Y i))" in exI)
   apply (rule conjI)
    apply (rule chain_monofun)
-   apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
+   apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
   apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
   apply (drule less_sinlD, clarify)
   apply (simp add: sinl_eq Rep_Ssum_sinl)
@@ -156,7 +156,7 @@
  apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI)
  apply (rule conjI)
   apply (rule chain_monofun)
-  apply (erule cont_Rep_Ssum [THEN cont2mono, THEN ch2ch_monofun])
+  apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
  apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
  apply (drule less_sinrD, clarify)
  apply (simp add: sinr_eq Rep_Ssum_sinr)
isabelle