1.1 --- a/src/HOLCF/Bifinite.thy	Fri Jun 20 22:51:50 2008 +0200
     1.2 +++ b/src/HOLCF/Bifinite.thy	Fri Jun 20 23:01:09 2008 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  class profinite = cpo +
     1.6    fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a"
     1.7 -  assumes chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
     1.8 +  assumes chain_approx [simp]: "chain approx"
     1.9    assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
    1.10    assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.11    assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
    1.12 @@ -27,13 +27,6 @@
    1.13  apply (clarify, erule subst, rule exI, rule refl)
    1.14  done
    1.15  
    1.16 -lemma chain_approx [simp]: "chain approx"
    1.17 -apply (rule chainI)
    1.18 -apply (rule less_cfun_ext)
    1.19 -apply (rule chainE)
    1.20 -apply (rule chain_approx_app)
    1.21 -done
    1.22 -
    1.23  lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
    1.24  by (rule ext_cfun, simp add: contlub_cfun_fun)
    1.25