changeset 43813 | 07f0650146f2 |
parent 43597 | b4a093e755db |
child 43814 | 58791b75cf1f |
--- 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"