src/HOL/Lattices.thy
changeset 22068 00bed5ac9884
parent 21734 283461c15fa7
child 22139 539a63b98f76
     1.1 --- a/src/HOL/Lattices.thy	Tue Jan 16 08:06:55 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Tue Jan 16 08:06:57 2007 +0100
     1.3 @@ -16,12 +16,12 @@
     1.4  Finite_Set}. In the longer term it may be better to define arbitrary
     1.5  sups and infs via @{text THE}. *}
     1.6  
     1.7 -locale lower_semilattice = partial_order +
     1.8 +locale lower_semilattice = order +
     1.9    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.10    assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
    1.11    and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    1.12  
    1.13 -locale upper_semilattice = partial_order +
    1.14 +locale upper_semilattice = order +
    1.15    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.16    assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
    1.17    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"