--- a/NEWS Mon Aug 18 15:03:25 2014 +0200
+++ b/NEWS Mon Aug 18 17:19:58 2014 +0200
@@ -17,6 +17,28 @@
*** HOL ***
+* New (co)datatype package:
+ - Renamed theorems:
+ disc_corec ~> corec_disc
+ disc_corec_iff ~> corec_disc_iff
+ disc_exclude ~> distinct_disc
+ disc_exhaust ~> exhaust_disc
+ disc_map_iff ~> map_disc_iff
+ sel_corec ~> corec_sel
+ sel_exhaust ~> exhaust_sel
+ sel_map ~> map_sel
+ sel_set ~> set_sel
+ sel_split ~> split_sel
+ sel_split_asm ~> split_sel_asm
+ strong_coinduct ~> coinduct_strong
+ weak_case_cong ~> case_cong_weak
+ INCOMPATIBILITY.
+
+* Old datatype package:
+ - Renamed theorems:
+ weak_case_cong ~> case_cong_weak
+ INCOMPATIBILITY.
+
* Sledgehammer:
- Minimization is now always enabled by default.
Removed subcommand: