src/HOL/Lattices.thy
changeset 41082 9ff94e7cc3b3
parent 41080 294956ff285b
child 43753 fe5e846c0839
     1.1 --- a/src/HOL/Lattices.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Dec 08 15:05:46 2010 +0100
     1.3 @@ -48,8 +48,9 @@
     1.4  notation
     1.5    less_eq  (infix "\<sqsubseteq>" 50) and
     1.6    less  (infix "\<sqsubset>" 50) and
     1.7 -  top ("\<top>") and
     1.8 -  bot ("\<bottom>")
     1.9 +  bot ("\<bottom>") and
    1.10 +  top ("\<top>")
    1.11 +
    1.12  
    1.13  class semilattice_inf = order +
    1.14    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)