# HG changeset patch
# User blanchet
# Date 1473694329 -7200
# Node ID 40f34614bd06b83bc535e4628bb2a5a1412c41c1
# Parent  e90f51b20215c676a45a78a867b1803dbc13ddfe
NEWS

diff -r e90f51b20215 -r 40f34614bd06 NEWS
--- a/NEWS	Mon Sep 12 17:10:35 2016 +0200
+++ b/NEWS	Mon Sep 12 17:32:09 2016 +0200
@@ -326,21 +326,24 @@
     'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
     method. See 'isabelle doc corec'.
   - The predicator :: ('a => bool) => 'a F => bool is now a first-class
-    citizen in bounded natural functors
+    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' 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)
+       (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
+       (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.
   - The "size" plugin has been made compatible again with locales.
+  - The theorems about "rel" and "set" may have a slightly different (but
+    equivalent) form.
+    INCOMPATIBILITY.
 
 * Some old / obsolete theorems have been renamed / removed, potential
 INCOMPATIBILITY.