src/HOLCF/Bifinite.thy
changeset 27310 d0229bc6c461
parent 27309 c74270fd72a8
child 27402 253a06dfadce
--- a/src/HOLCF/Bifinite.thy	Fri Jun 20 22:51:50 2008 +0200
+++ b/src/HOLCF/Bifinite.thy	Fri Jun 20 23:01:09 2008 +0200
@@ -13,7 +13,7 @@
 
 class profinite = cpo +
   fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
-  assumes chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
+  assumes chain_approx [simp]: "chain approx"
   assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
   assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
@@ -27,13 +27,6 @@
 apply (clarify, erule subst, rule exI, rule refl)
 done
 
-lemma chain_approx [simp]: "chain approx"
-apply (rule chainI)
-apply (rule less_cfun_ext)
-apply (rule chainE)
-apply (rule chain_approx_app)
-done
-
 lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
 by (rule ext_cfun, simp add: contlub_cfun_fun)