
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 ..




