[isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases

[Alexander Krauss]

This refers to Isabelle f557a4645f61:

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

Contributed by Manuel Eberl.