--- a/NEWS Wed Jul 13 19:43:12 2011 +0200
+++ b/NEWS Wed Jul 13 23:41:13 2011 +0200
@@ -60,6 +60,9 @@
*** HOL ***
+* classes bot and top require underlying partial order rather than preorder:
+uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
+
* Archimedian_Field.thy:
floor now is defined as parameter of a separate type class floor_ceiling.
--- a/src/HOL/Library/Option_ord.thy Wed Jul 13 19:43:12 2011 +0200
+++ b/src/HOL/Library/Option_ord.thy Wed Jul 13 23:41:13 2011 +0200
@@ -58,7 +58,7 @@
instance option :: (linorder) linorder proof
qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
-instantiation option :: (preorder) bot
+instantiation option :: (order) bot
begin
definition "bot = None"
--- a/src/HOL/Library/Quickcheck_Types.thy Wed Jul 13 19:43:12 2011 +0200
+++ b/src/HOL/Library/Quickcheck_Types.thy Wed Jul 13 23:41:13 2011 +0200
@@ -108,7 +108,7 @@
instance bot :: (linorder) linorder proof
qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
-instantiation bot :: (preorder) bot
+instantiation bot :: (order) bot
begin
definition "bot = Bot"
@@ -208,7 +208,7 @@
instance top :: (linorder) linorder proof
qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
-instantiation top :: (preorder) top
+instantiation top :: (order) top
begin
definition "top = Top"