# HG changeset patch
# User krauss
# Date 1378838072 -7200
# Node ID cdc780645a49203b71877838dc042c4bef62fe0d
# Parent  c9d6f6285e1dd0d14f3dbb953d25e5d4bdec93fe
NEWS and CONTRIBUTORS

diff -r c9d6f6285e1d -r cdc780645a49 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Sep 10 20:11:01 2013 +0200
+++ b/CONTRIBUTORS	Tue Sep 10 20:34:32 2013 +0200
@@ -9,6 +9,10 @@
 * September 2013: Nik Sultana, University of Cambridge
   Improvements to HOL/TPTP parser and import facilities.
 
+* Summer 2013: Manuel Eberl, TUM
+  Generation of elimination rules in the function package.
+  New command "fun_cases".
+
 * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and
   Jasmin Blanchette, TUM
   Various improvements to BNF-based (co)datatype package, including a
diff -r c9d6f6285e1d -r cdc780645a49 NEWS
--- a/NEWS	Tue Sep 10 20:11:01 2013 +0200
+++ b/NEWS	Tue Sep 10 20:34:32 2013 +0200
@@ -193,6 +193,19 @@
     set_map' ~> set_map
 IMCOMPATIBILITY.
 
+* Function package: For mutually recursive functions f and g, separate
+cases rules f.cases and g.cases are generated instead of unusable
+f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
+in the case that the unusable rule was used nevertheless.
+
+* Function package: For each function f, new rules f.elims are
+automatically generated, which eliminate equalities of the form "f x =
+t".
+
+* New command "fun_cases" derives ad-hoc elimination rules for
+function equations as simplified instances of f.elims, analogous to
+inductive_cases.  See HOL/ex/Fundefs.thy for some examples.
+
 * Library/Polynomial.thy:
   - Use lifting for primitive definitions.
   - Explicit conversions from and to lists of coefficients, used for