NEWS
changeset 53613 cdc780645a49
parent 53398 f8b150e8778b
child 53615 f557a4645f61
equal deleted 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.