| changeset 21326 | c33cdc5a6c7c |
| parent 21316 | 4d913b8bccf1 |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/FixedPoint.thy Mon Nov 13 15:43:00 2006 +0100 +++ b/src/HOL/FixedPoint.thy Mon Nov 13 15:43:03 2006 +0100 @@ -8,7 +8,7 @@ header{* Fixed Points and the Knaster-Tarski Theorem*} theory FixedPoint -imports Product_Type +imports Product_Type LOrder begin subsection {* Complete lattices *}