src/HOL/Lattice/Lattice.thy

 (*  Title:      HOL/Lattice/Lattice.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Lattices *}
 

   A \emph{lattice} is a partial order with infimum and supremum of any
   two elements (thus any \emph{finite} number of elements have bounds
   as well).
 *}
 
-axclass lattice \<subseteq> partial_order
-  ex_inf: "\<exists>inf. is_inf x y inf"
-  ex_sup: "\<exists>sup. is_sup x y sup"
+class lattice =
+  assumes ex_inf: "\<exists>inf. is_inf x y inf"
+  assumes ex_sup: "\<exists>sup. is_sup x y sup"
 
 text {*
   The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such
   infimum and supremum elements.
 *}