diff -r 470b579f35d2 -r 412c9e0381a1 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Wed Jul 24 17:15:59 2013 +0200 +++ b/src/HOL/Lattices.thy Thu Jul 25 08:57:16 2013 +0200 @@ -466,7 +466,7 @@ subsection {* Bounded lattices and boolean algebras *} -class bounded_semilattice_inf_top = semilattice_inf + top +class bounded_semilattice_inf_top = semilattice_inf + order_top begin sublocale inf_top!: semilattice_neutr inf top @@ -479,7 +479,7 @@ end -class bounded_semilattice_sup_bot = semilattice_sup + bot +class bounded_semilattice_sup_bot = semilattice_sup + order_bot begin sublocale sup_bot!: semilattice_neutr sup bot @@ -492,7 +492,7 @@ end -class bounded_lattice_bot = lattice + bot +class bounded_lattice_bot = lattice + order_bot begin subclass bounded_semilattice_sup_bot .. @@ -523,7 +523,7 @@ end -class bounded_lattice_top = lattice + top +class bounded_lattice_top = lattice + order_top begin subclass bounded_semilattice_inf_top .. @@ -550,7 +550,7 @@ end -class bounded_lattice = lattice + bot + top +class bounded_lattice = lattice + order_bot + order_top begin subclass bounded_lattice_bot ..