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/Library/Defl_Bifinite.thy
changeset 40002 c5b5f7a3a3b1
parent 39999 e3948547b541
child 40491 6de5839e2fb3 
--- a/src/HOLCF/Library/Defl_Bifinite.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Library/Defl_Bifinite.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -240,7 +240,7 @@
   hence "MOST i. MOST j. \<forall>x. iterate (Suc j)\<cdot>f\<cdot>x = iterate (Suc i)\<cdot>f\<cdot>x"
     by (simp only: iterate_Suc2)
   hence "MOST i. MOST j. iterate (Suc j)\<cdot>f = iterate (Suc i)\<cdot>f"
-    by (simp only: expand_cfun_eq)
+    by (simp only: cfun_eq_iff)
   hence "eventually_constant (\<lambda>i. iterate (Suc i)\<cdot>f)"
     unfolding eventually_constant_MOST_MOST .
   thus "eventually_constant (\<lambda>i. iterate i\<cdot>f)"
@@ -587,7 +587,7 @@
     apply (simp add: defl_approx_principal fd_take_below)
     done
   show lub: "(\<Squnion>i. defl_approx i) = ID"
-    apply (rule ext_cfun, rule below_antisym)
+    apply (rule cfun_eqI, rule below_antisym)
     apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
     apply (induct_tac x rule: defl.principal_induct, simp)
     apply (simp add: contlub_cfun_fun chain)
isabelle