Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Ssum.thy
changeset 16742 d1641dba61e5
parent 16699 24b494ff8f0f
child 16752 270ec60cc9e8 
--- 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