1.1 --- a/src/HOLCF/Fix.thy	Sat Jan 16 17:15:28 2010 +0100
     1.2 +++ b/src/HOLCF/Fix.thy	Sun Feb 07 10:15:15 2010 -0800
     1.3 @@ -73,6 +73,10 @@
     1.4  apply simp
     1.5  done
     1.6  
     1.7 +lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
     1.8 +  unfolding fix_def2
     1.9 +  using chain_iterate by (rule is_ub_thelub)
    1.10 +
    1.11  text {*
    1.12    Kleene's fixed point theorems for continuous functions in pointed
    1.13    omega cpo's