1.1 --- a/src/HOLCF/Bifinite.thy	Tue Sep 16 12:25:04 2008 +0200
     1.2 +++ b/src/HOLCF/Bifinite.thy	Tue Sep 16 12:25:26 2008 +0200
     1.3 @@ -41,8 +41,10 @@
     1.4  interpretation approx: finite_deflation ["approx i"]
     1.5  by (rule finite_deflation_approx)
     1.6  
     1.7 +lemma (in deflation) deflation: "deflation d" ..
     1.8 +
     1.9  lemma deflation_approx: "deflation (approx i)"
    1.10 -by (rule approx.deflation_axioms)
    1.11 +by (rule approx.deflation)
    1.12  
    1.13  lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
    1.14  by (rule ext_cfun, simp add: contlub_cfun_fun)