document addition of 'corec'
authorblanchet
Tue Mar 22 12:39:37 2016 +0100 (2016-03-22)
changeset 626930ae225877b68
parent 62692 0701f25fac39
child 62694 f50d7efc8fe3
document addition of 'corec'
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Mar 22 12:39:37 2016 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -20,9 +20,14 @@
     1.4  Contributions to Isabelle2016
     1.5  -----------------------------
     1.6  
     1.7 +* Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy,
     1.8 +  Ecole polytechnique, Andreas Lochbihler, ETH Zurich, and Dmitriy Traytel,
     1.9 +  ETH Zurich
    1.10 +  'corec' command and friends.
    1.11 +
    1.12  * Winter 2016: Manuel Eberl, TUM
    1.13    Support for real exponentiation ("powr") in the "approximation" method.
    1.14 -  (This was removed in Isabelle 2015 due to a changed definition of "powr")
    1.15 +  (This was removed in Isabelle 2015 due to a changed definition of "powr".)
    1.16  
    1.17  * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge
    1.18    General, homology form of Cauchy's integral theorem and supporting material
     2.1 --- a/NEWS	Tue Mar 22 12:39:37 2016 +0100
     2.2 +++ b/NEWS	Tue Mar 22 12:39:37 2016 +0100
     2.3 @@ -33,17 +33,21 @@
     2.4  eliminated altogether.
     2.5  
     2.6  * (Co)datatype package:
     2.7 -  - the predicator :: ('a => bool) => 'a F => bool is now a first-class
     2.8 +  - New commands for defining corecursive functions and reasoning about
     2.9 +    them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
    2.10 +    'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
    2.11 +    method.
    2.12 +  - The predicator :: ('a => bool) => 'a F => bool is now a first-class
    2.13      citizen in bounded natural functors
    2.14 -  - "primrec" now allows nested calls through the predicator in addition
    2.15 +  - 'primrec' now allows nested calls through the predicator in addition
    2.16      to the map function.
    2.17 -  - "bnf" automatically discharges reflexive proof obligations
    2.18 -    "bnf" outputs a slightly modified proof obligation expressing rel in
    2.19 +  - 'bnf' automatically discharges reflexive proof obligations
    2.20 +  - 'bnf' outputs a slightly modified proof obligation expressing rel in
    2.21         terms of map and set
    2.22         (not giving a specification for rel makes this one reflexive)
    2.23 -    "bnf" outputs a new proof obligation expressing pred in terms of set
    2.24 +  - 'bnf' outputs a new proof obligation expressing pred in terms of set
    2.25         (not giving a specification for pred makes this one reflexive)
    2.26 -    INCOMPATIBILITY: manual "bnf" declarations may need adjustment
    2.27 +    INCOMPATIBILITY: manual 'bnf' declarations may need adjustment
    2.28    - Renamed lemmas:
    2.29        rel_prod_apply ~> rel_prod_inject
    2.30        pred_prod_apply ~> pred_prod_inject