tightened specification of classes bot and top: uniqueness of top and bot elements

--- a/src/HOL/Orderings.thy	Wed Jul 13 18:36:11 2011 +0200
+++ b/src/HOL/Orderings.thy	Wed Jul 13 19:40:18 2011 +0200
@@ -1081,13 +1081,13 @@
 done
 
 
-subsection {* Top and bottom elements *}
+subsection {* (Unique) top and bottom elements *}
 
-class bot = preorder +
+class bot = order +
   fixes bot :: 'a
   assumes bot_least [simp]: "bot \<le> x"
 
-class top = preorder +
+class top = order +
   fixes top :: 'a
   assumes top_greatest [simp]: "x \<le> top"