1.1 --- a/NEWS	Thu Apr 19 22:13:46 2012 +0200
     1.2 +++ b/NEWS	Thu Apr 19 22:21:15 2012 +0200
     1.3 @@ -475,6 +475,15 @@
     1.4    unionwk_is_rbt -> rbt_unionwk_is_rbt
     1.5    unionwk_sorted -> rbt_unionwk_rbt_sorted
     1.6  
     1.7 +* Theory HOL/Library/Float: Floating point numbers are now defined as a
     1.8 +subset of the real numbers. All operations are defined using the
     1.9 +lifing-framework and most proofs use the transfer method.
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12 +  Changed Operations:
    1.13 +  scale   ~>   exponent
    1.14 +  pow2 x  ~>   use "2 powr (real x)"
    1.15 +
    1.16  * Session HOL-Word: Discontinued many redundant theorems specific to
    1.17  type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
    1.18  instead.