diff -r 15176172701e -r e85c42f4f30a NEWS
--- a/NEWS	Wed Feb 17 17:08:03 2016 +0100
+++ b/NEWS	Wed Feb 17 17:08:36 2016 +0100
@@ -27,6 +27,10 @@
     "bnf" outputs a new proof obligation expressing pred in terms of set
        (not giving a specification for pred makes this one reflexive)
     INCOMPATIBILITY: manual "bnf" declarations may need adjustment
+  - Renamed lemmas:
+      rel_prod_apply ~> rel_prod_inject
+      pred_prod_apply ~> pred_prod_inject
+    INCOMPATIBILITY.
 
 
 New in Isabelle2016 (February 2016)