src/HOL/Library/Finite_Lattice.thy

 (* Author: Alessandro Coglio *)
 
 theory Finite_Lattice
-imports Product_Lattice
+imports Product_Order
 begin
 
 text {* A non-empty finite lattice is a complete lattice.
 Since types are never empty in Isabelle/HOL,
 a type of classes @{class finite} and @{class lattice}