# HG changeset patch
# User traytel
# Date 1455720088 -3600
# Node ID eeaa2f7b53296f685e0cf1e95d76ceda3435e891
# Parent  e923f200bda5bb23bcfef75f2d916c7a3b189669
NEWS

diff -r e923f200bda5 -r eeaa2f7b5329 NEWS
--- a/NEWS	Wed Feb 17 15:18:06 2016 +0100
+++ b/NEWS	Wed Feb 17 15:41:28 2016 +0100
@@ -16,8 +16,17 @@
 *** HOL ***
 
 * (Co)datatype package:
+  - the predicator :: ('a => bool) => 'a F => bool is now a first-class
+    citizen in bounded natural functors
   - "primrec" now allows nested calls through the predicator in addition
     to the map function.
+  - "bnf" automatically discharges reflexive proof obligations
+    "bnf" outputs a slightly modified proof obligation expressing rel in
+       terms of map and set
+       (not giving a specification for rel makes this one reflexive)
+    "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
 
 
 New in Isabelle2016 (February 2016)