changeset 24164 | 911b46812018 |
parent 23948 | 261bd4678076 |
child 24345 | 86a3557a9ebb |
--- a/src/HOL/Lattices.thy Tue Aug 07 09:38:46 2007 +0200 +++ b/src/HOL/Lattices.thy Tue Aug 07 09:38:47 2007 +0200 @@ -225,7 +225,7 @@ end -subsection{* Distributive lattices *} +subsection {* Distributive lattices *} class distrib_lattice = lattice + assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"