# HG changeset patch
# User hoelzl
# Date 1334866875 -7200
# Node ID 632a1e5710e6842fc4e6404ff80683826b15e230
# Parent  341fd902ef1ceb57906eb6a9f322933c80daf95b
NEWS

diff -r 341fd902ef1c -r 632a1e5710e6 NEWS
--- a/NEWS	Thu Apr 19 22:13:46 2012 +0200
+++ b/NEWS	Thu Apr 19 22:21:15 2012 +0200
@@ -475,6 +475,15 @@
   unionwk_is_rbt -> rbt_unionwk_is_rbt
   unionwk_sorted -> rbt_unionwk_rbt_sorted
 
+* Theory HOL/Library/Float: Floating point numbers are now defined as a
+subset of the real numbers. All operations are defined using the
+lifing-framework and most proofs use the transfer method.
+INCOMPATIBILITY.
+
+  Changed Operations:
+  scale   ~>   exponent
+  pow2 x  ~>   use "2 powr (real x)"
+
 * Session HOL-Word: Discontinued many redundant theorems specific to
 type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
 instead.