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/Up.thy
changeset 40771 1c6f7d4b110e
parent 40502 8e92772bc0e8 
--- a/src/HOLCF/Up.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Up.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -111,7 +111,7 @@
   proof (rule up_chain_lemma)
     assume "\<forall>i. S i = Ibottom"
     hence "range (\<lambda>i. S i) <<| Ibottom"
-      by (simp add: lub_const)
+      by (simp add: is_lub_const)
     thus ?thesis ..
   next
     fix A :: "nat \<Rightarrow> 'a"
@@ -160,7 +160,7 @@
     assume A: "\<forall>i. Iup (A i) = Y (i + k)"
     assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)"
     hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))"
-      by (simp add: thelubI contlub_cfun_arg)
+      by (simp add: lub_eqI contlub_cfun_arg)
     also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))"
       by (simp add: A)
     also have "\<dots> = (\<Squnion>i. Ifup f (Y i))"
@@ -223,7 +223,7 @@
   assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>"
   | A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)"
 apply (rule up_chain_lemma [OF Y])
-apply (simp_all add: inst_up_pcpo up_def cont_Iup thelubI)
+apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI)
 done
 
 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)"
isabelle