# HG changeset patch
# User haftmann
# Date 1310578818 -7200
# Node ID 07f0650146f29495c23ee1b01957c04b251fbfbf
# Parent  534c5eb522a6cde7ad4ce987de13185d757c1d80
tightened specification of classes bot and top: uniqueness of top and bot elements

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 \<le> x"
 
-class top = preorder +
+class top = order +
   fixes top :: 'a
   assumes top_greatest [simp]: "x \<le> top"