document addition of 'corec'
authorblanchet
Tue, 22 Mar 2016 12:39:37 +0100
changeset 62693 0ae225877b68
parent 62692 0701f25fac39
child 62694 f50d7efc8fe3
document addition of 'corec'
CONTRIBUTORS
NEWS
--- 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