--- 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
--- 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