1.1 --- a/src/HOLCF/Bifinite.thy	Thu Jan 17 21:44:19 2008 +0100
     1.2 +++ b/src/HOLCF/Bifinite.thy	Thu Jan 17 21:56:33 2008 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4    fixes x y :: "'a::bifinite_cpo"
     1.5    shows "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
     1.6  apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
     1.7 -apply (rule lub_mono [rule_format], simp, simp, simp)
     1.8 +apply (rule lub_mono, simp, simp, simp)
     1.9  done
    1.10  
    1.11  subsection {* Instance for continuous function space *}