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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
