NEWS
changeset 57983 6edc3529bb4e
parent 57946 6a26aa5fa65e
child 57990 90d941a477bd
     1.1 --- a/NEWS	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/NEWS	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -17,6 +17,28 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New (co)datatype package:
     1.8 +  - Renamed theorems:
     1.9 +      disc_corec ~> corec_disc
    1.10 +      disc_corec_iff ~> corec_disc_iff
    1.11 +      disc_exclude ~> distinct_disc
    1.12 +      disc_exhaust ~> exhaust_disc
    1.13 +      disc_map_iff ~> map_disc_iff
    1.14 +      sel_corec ~> corec_sel
    1.15 +      sel_exhaust ~> exhaust_sel
    1.16 +      sel_map ~> map_sel
    1.17 +      sel_set ~> set_sel
    1.18 +      sel_split ~> split_sel
    1.19 +      sel_split_asm ~> split_sel_asm
    1.20 +      strong_coinduct ~> coinduct_strong
    1.21 +      weak_case_cong ~> case_cong_weak
    1.22 +    INCOMPATIBILITY.
    1.23 +
    1.24 +* Old datatype package:
    1.25 +  - Renamed theorems:
    1.26 +      weak_case_cong ~> case_cong_weak
    1.27 +    INCOMPATIBILITY.
    1.28 +
    1.29  * Sledgehammer:
    1.30    - Minimization is now always enabled by default.
    1.31      Removed subcommand: