| changeset 40500 | ee9c8d36318e |
| parent 40321 | d065b195ec89 |
| child 40771 | 1c6f7d4b110e |
--- a/src/HOLCF/Fix.thy Wed Nov 10 13:22:39 2010 -0800 +++ b/src/HOLCF/Fix.thy Wed Nov 10 14:20:47 2010 -0800 @@ -82,9 +82,8 @@ lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x" apply (simp add: fix_def2) -apply (rule is_lub_thelub) +apply (rule lub_below) apply (rule chain_iterate) -apply (rule ub_rangeI) apply (induct_tac i) apply simp apply simp