diff -r 534c5eb522a6 -r 07f0650146f2 src/HOL/Orderings.thy --- 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 \ x" -class top = preorder + +class top = order + fixes top :: 'a assumes top_greatest [simp]: "x \ top"