[isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases
krauss at in.tum.de
Fri Sep 13 17:16:24 CEST 2013
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 =
* 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.
More information about the isabelle-dev