changeset 53613 cdc780645a49
parent 53398 f8b150e8778b
child 53615 f557a4645f61
--- 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
+* 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 =
+* 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