*** HOL *** * SUP and INF generalized to conditionally_complete_lattice * Theory Lubs moved from HOL image to HOL-Library. It is replaced by Conditionally_Complete_Lattices. INCOMPATIBILITY. * Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them instead of explicitly stating boundedness of sets.