diff -r a2b7993a0529 -r c3f2e9986e30 NEWS
--- a/NEWS	Wed Aug 18 12:27:39 2010 +0200
+++ b/NEWS	Wed Aug 18 14:55:09 2010 +0200
@@ -77,6 +77,8 @@
     nat ~> Nat.nat
 
   constants
+    Let ~> HOL.Let
+    If ~> HOL.If
     Ball ~> Set.Ball
     Bex ~> Set.Bex
     Suc ~> Nat.Suc
@@ -90,7 +92,7 @@
 INCOMPATIBILITY.
 
 * Removed simplifier congruence rule of "prod_case", as has for long
-been the case with "split".
+been the case with "split".  INCOMPATIBILITY.
 
 * Datatype package: theorems generated for executable equality
 (class eq) carry proper names and are treated as default code
@@ -99,8 +101,8 @@
 * List.thy: use various operations from the Haskell prelude when
 generating Haskell code.
 
-* code_simp.ML: simplification with rules determined by
-code generator.
+* code_simp.ML and method code_simp: simplification with rules determined
+by code generator.
 
 * code generator: do not print function definitions for case
 combinators any longer.