1.1 --- a/NEWS	Wed Jul 13 19:43:12 2011 +0200
     1.2 +++ b/NEWS	Wed Jul 13 23:41:13 2011 +0200
     1.3 @@ -60,6 +60,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* classes bot and top require underlying partial order rather than preorder:
     1.8 +uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
     1.9 +
    1.10  * Archimedian_Field.thy:
    1.11      floor now is defined as parameter of a separate type class floor_ceiling.
    1.12   

     2.1 --- a/src/HOL/Library/Option_ord.thy	Wed Jul 13 19:43:12 2011 +0200
     2.2 +++ b/src/HOL/Library/Option_ord.thy	Wed Jul 13 23:41:13 2011 +0200
     2.3 @@ -58,7 +58,7 @@
     2.4  instance option :: (linorder) linorder proof
     2.5  qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
     2.6  
     2.7 -instantiation option :: (preorder) bot
     2.8 +instantiation option :: (order) bot
     2.9  begin
    2.10  
    2.11  definition "bot = None"

     3.1 --- a/src/HOL/Library/Quickcheck_Types.thy	Wed Jul 13 19:43:12 2011 +0200
     3.2 +++ b/src/HOL/Library/Quickcheck_Types.thy	Wed Jul 13 23:41:13 2011 +0200
     3.3 @@ -108,7 +108,7 @@
     3.4  instance bot :: (linorder) linorder proof
     3.5  qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
     3.6  
     3.7 -instantiation bot :: (preorder) bot
     3.8 +instantiation bot :: (order) bot
     3.9  begin
    3.10  
    3.11  definition "bot = Bot"
    3.12 @@ -208,7 +208,7 @@
    3.13  instance top :: (linorder) linorder proof
    3.14  qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
    3.15  
    3.16 -instantiation top :: (preorder) top
    3.17 +instantiation top :: (order) top
    3.18  begin
    3.19  
    3.20  definition "top = Top"