src/HOL/Lattice/CompleteLattice.thy
changeset 10176 2e38e3c94990
parent 10175 76646fc8b1bf
child 10183 76f0f0f1c971
equal deleted 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