src/HOL/Lattices.thy
changeset 51546 2e26df807dc7
parent 51540 eea5c4ca4a0e
child 51593 d40aec502416
     1.1 --- a/src/HOL/Lattices.thy	Tue Mar 26 20:55:21 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Tue Mar 26 21:53:56 2013 +0100
     1.3 @@ -471,25 +471,23 @@
     1.4  class bounded_semilattice_inf_top = semilattice_inf + top
     1.5  
     1.6  sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
     1.7 +  + inf_top!: semilattice_neutr_order inf top less_eq less
     1.8  proof
     1.9    fix x
    1.10    show "x \<sqinter> \<top> = x"
    1.11      by (rule inf_absorb1) simp
    1.12  qed
    1.13  
    1.14 -sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
    1.15 -
    1.16  class bounded_semilattice_sup_bot = semilattice_sup + bot
    1.17  
    1.18  sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
    1.19 +  + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
    1.20  proof
    1.21    fix x
    1.22    show "x \<squnion> \<bottom> = x"
    1.23      by (rule sup_absorb1) simp
    1.24  qed
    1.25  
    1.26 -sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
    1.27 -
    1.28  class bounded_lattice_bot = lattice + bot
    1.29  begin
    1.30