author | krauss |

Tue Sep 10 20:34:32 2013 +0200 (2013-09-10 ago) | |

changeset 53613 | cdc780645a49 |

parent 53612 | c9d6f6285e1d |

child 53614 | 8c51fc24d83c |

NEWS and CONTRIBUTORS

1.1 --- a/CONTRIBUTORS Tue Sep 10 20:11:01 2013 +0200 1.2 +++ b/CONTRIBUTORS Tue Sep 10 20:34:32 2013 +0200 1.3 @@ -9,6 +9,10 @@ 1.4 * September 2013: Nik Sultana, University of Cambridge 1.5 Improvements to HOL/TPTP parser and import facilities. 1.6 1.7 +* Summer 2013: Manuel Eberl, TUM 1.8 + Generation of elimination rules in the function package. 1.9 + New command "fun_cases". 1.10 + 1.11 * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and 1.12 Jasmin Blanchette, TUM 1.13 Various improvements to BNF-based (co)datatype package, including a

2.1 --- a/NEWS Tue Sep 10 20:11:01 2013 +0200 2.2 +++ b/NEWS Tue Sep 10 20:34:32 2013 +0200 2.3 @@ -193,6 +193,19 @@ 2.4 set_map' ~> set_map 2.5 IMCOMPATIBILITY. 2.6 2.7 +* Function package: For mutually recursive functions f and g, separate 2.8 +cases rules f.cases and g.cases are generated instead of unusable 2.9 +f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY, 2.10 +in the case that the unusable rule was used nevertheless. 2.11 + 2.12 +* Function package: For each function f, new rules f.elims are 2.13 +automatically generated, which eliminate equalities of the form "f x = 2.14 +t". 2.15 + 2.16 +* New command "fun_cases" derives ad-hoc elimination rules for 2.17 +function equations as simplified instances of f.elims, analogous to 2.18 +inductive_cases. See HOL/ex/Fundefs.thy for some examples. 2.19 + 2.20 * Library/Polynomial.thy: 2.21 - Use lifting for primitive definitions. 2.22 - Explicit conversions from and to lists of coefficients, used for