author | blanchet |

Tue Mar 22 12:39:37 2016 +0100 (2016-03-22) | |

changeset 62693 | 0ae225877b68 |

parent 62692 | 0701f25fac39 |

child 62694 | f50d7efc8fe3 |

document addition of 'corec'

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