tuned;
authorwenzelm
Sun Jan 24 12:33:09 2016 +0100 (2016-01-24)
changeset 622353687c199e22b
parent 62234 7cc9d7b822ae
child 62236 3a326bc9d4d8
tuned;
NEWS
     1.1 --- a/NEWS	Sun Jan 24 12:21:57 2016 +0100
     1.2 +++ b/NEWS	Sun Jan 24 12:33:09 2016 +0100
     1.3 @@ -594,8 +594,8 @@
     1.4    - New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
     1.5      structure on the raw type to an abstract type defined using typedef.
     1.6    - Always generate "case_transfer" theorem.
     1.7 -  - For mutual types, generate slightly stronger "rel_induct", "rel_coinduct",
     1.8 -    and "coinduct" theorems. INCOMPATIBLITY.
     1.9 +  - For mutual types, generate slightly stronger "rel_induct",
    1.10 +    "rel_coinduct", and "coinduct" theorems. INCOMPATIBLITY.
    1.11    - Allow discriminators and selectors with the same name as the type
    1.12      being defined.
    1.13    - Avoid various internal name clashes (e.g., 'datatype f = f').
    1.14 @@ -682,8 +682,8 @@
    1.15        less_eq_multiset.rep_eq ~> subseteq_mset_def
    1.16      INCOMPATIBILITY
    1.17    - Removed lemmas generated by lift_definition:
    1.18 -    less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer
    1.19 -    less_eq_multiset_def
    1.20 +    less_eq_multiset.abs_eq, less_eq_multiset.rsp,
    1.21 +    less_eq_multiset.transfer, less_eq_multiset_def
    1.22      INCOMPATIBILITY
    1.23  
    1.24  * Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.