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.