--- 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.