NEWS and CONTRIBUTORS
authorkrauss
Tue Sep 10 20:34:32 2013 +0200 (2013-09-10)
changeset 53613cdc780645a49
parent 53612 c9d6f6285e1d
child 53614 8c51fc24d83c
NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     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