NEWS
changeset 43815 4f6e2965d821
parent 43752 0517a69de5d6
child 43816 05ab37be94ed
--- 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.