# HG changeset patch
# User haftmann
# Date 1310593273 -7200
# Node ID 4f6e2965d82172ec71c352a76dde1307f6e14dc3
# Parent  58791b75cf1f6d9908c731d7f1bc0e2a2c094ad6
adjusted to tightened specification of classes bot and top

diff -r 58791b75cf1f -r 4f6e2965d821 NEWS
--- 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.
  
diff -r 58791b75cf1f -r 4f6e2965d821 src/HOL/Library/Option_ord.thy
--- 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"
diff -r 58791b75cf1f -r 4f6e2965d821 src/HOL/Library/Quickcheck_Types.thy
--- 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"