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/Fix.thy
changeset 40771 1c6f7d4b110e
parent 40500 ee9c8d36318e 
--- a/src/HOLCF/Fix.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/Fix.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -183,7 +183,7 @@
   hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
     by - (rule admD [OF adm'], simp, assumption)
   hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
-    by (simp add: thelub_Pair)
+    by (simp add: lub_Pair)
   hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
     by simp
   thus "P (fix\<cdot>F) (fix\<cdot>G)"
isabelle