NEWS
 changeset 53613 cdc780645a49 parent 53398 f8b150e8778b child 53615 f557a4645f61
equal inserted replaced
53612:c9d6f6285e1d 53613:cdc780645a49
`   190   - Renamed many generated theorems, including`
`   190   - Renamed many generated theorems, including`
`   191     map_comp' ~> map_comp`
`   191     map_comp' ~> map_comp`
`   192     map_id' ~> map_id`
`   192     map_id' ~> map_id`
`   193     set_map' ~> set_map`
`   193     set_map' ~> set_map`
`   194 IMCOMPATIBILITY.`
`   194 IMCOMPATIBILITY.`
`       `
`   195 `
`       `
`   196 * Function package: For mutually recursive functions f and g, separate`
`       `
`   197 cases rules f.cases and g.cases are generated instead of unusable`
`       `
`   198 f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,`
`       `
`   199 in the case that the unusable rule was used nevertheless.`
`       `
`   200 `
`       `
`   201 * Function package: For each function f, new rules f.elims are`
`       `
`   202 automatically generated, which eliminate equalities of the form "f x =`
`       `
`   203 t".`
`       `
`   204 `
`       `
`   205 * New command "fun_cases" derives ad-hoc elimination rules for`
`       `
`   206 function equations as simplified instances of f.elims, analogous to`
`       `
`   207 inductive_cases.  See HOL/ex/Fundefs.thy for some examples.`
`   195 `
`   208 `
`   196 * Library/Polynomial.thy:`
`   209 * Library/Polynomial.thy:`
`   197   - Use lifting for primitive definitions.`
`   210   - Use lifting for primitive definitions.`
`   198   - Explicit conversions from and to lists of coefficients, used for`
`   211   - Explicit conversions from and to lists of coefficients, used for`
`   199     generated code.`
`   212     generated code.`