| changeset 21316 | 4d913b8bccf1 |
| parent 21312 | 1d39091a3208 |
| child 21326 | c33cdc5a6c7c |
--- a/src/HOL/FixedPoint.thy Sun Nov 12 21:14:52 2006 +0100 +++ b/src/HOL/FixedPoint.thy Sun Nov 12 21:31:52 2006 +0100 @@ -112,7 +112,7 @@ done lemma SUP_const[simp]: "(SUP i. M) = (M::'a::comp_lat)" -by(simp add:SUP_def join_absorp1) +by(simp add:SUP_def image_constant_conv join_absorp1) subsection {* Some instances of the type class of complete lattices *}