--- a/CONTRIBUTORS Tue Mar 22 12:39:37 2016 +0100
+++ b/CONTRIBUTORS Tue Mar 22 12:39:37 2016 +0100
@@ -20,9 +20,14 @@
Contributions to Isabelle2016
-----------------------------
+* Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy,
+ Ecole polytechnique, Andreas Lochbihler, ETH Zurich, and Dmitriy Traytel,
+ ETH Zurich
+ 'corec' command and friends.
+
* Winter 2016: Manuel Eberl, TUM
Support for real exponentiation ("powr") in the "approximation" method.
- (This was removed in Isabelle 2015 due to a changed definition of "powr")
+ (This was removed in Isabelle 2015 due to a changed definition of "powr".)
* Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
General, homology form of Cauchy's integral theorem and supporting material
--- a/NEWS Tue Mar 22 12:39:37 2016 +0100
+++ b/NEWS Tue Mar 22 12:39:37 2016 +0100
@@ -33,17 +33,21 @@
eliminated altogether.
* (Co)datatype package:
- - the predicator :: ('a => bool) => 'a F => bool is now a first-class
+ - New commands for defining corecursive functions and reasoning about
+ them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
+ 'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
+ method.
+ - 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
+ - '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
+ - '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
+ - '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
+ INCOMPATIBILITY: manual 'bnf' declarations may need adjustment
- Renamed lemmas:
rel_prod_apply ~> rel_prod_inject
pred_prod_apply ~> pred_prod_inject