1.1 --- a/src/HOL/Orderings.thy	Wed Jul 13 18:36:11 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Jul 13 19:40:18 2011 +0200
     1.3 @@ -1081,13 +1081,13 @@
     1.4  done
     1.5  
     1.6  
     1.7 -subsection {* Top and bottom elements *}
     1.8 +subsection {* (Unique) top and bottom elements *}
     1.9  
    1.10 -class bot = preorder +
    1.11 +class bot = order +
    1.12    fixes bot :: 'a
    1.13    assumes bot_least [simp]: "bot \<le> x"
    1.14  
    1.15 -class top = preorder +
    1.16 +class top = order +
    1.17    fixes top :: 'a
    1.18    assumes top_greatest [simp]: "x \<le> top"
    1.19