HOL.Complete_Lattices