src/HOL/Lattice/CompleteLattice.thy
 changeset 10176 2e38e3c94990 parent 10175 76646fc8b1bf child 10183 76f0f0f1c971
equal inserted replaced
10175:76646fc8b1bf 10176:2e38e3c94990
   254
   254
   255
   255
   256 subsection {* Complete lattices are lattices *}
   256 subsection {* Complete lattices are lattices *}
   257
   257
   258 text {*
   258 text {*
   259   Complete lattices (with general bounds) available are indeed plain
   259   Complete lattices (with general bounds available) are indeed plain
   260   lattices as well.  This holds due to the connection of general
   260   lattices as well.  This holds due to the connection of general
   261   versus binary bounds that has been formally established in
   261   versus binary bounds that has been formally established in
   262   \S\ref{sec:gen-bin-bounds}.
   262   \S\ref{sec:gen-bin-bounds}.
   263 *}
   263 *}
   264
   264