--- a/NEWS Tue Jun 10 23:28:42 2008 +0200
+++ b/NEWS Tue Jun 10 23:45:51 2008 +0200
@@ -7,7 +7,7 @@
*** Pure ***
* Command 'instance': attached definitions now longer accepted.
-INCOMPATIBILITY.
+INCOMPATIBILITY, use proper 'instantiation' target.
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY.
@@ -21,6 +21,8 @@
tuple elimination instead of former prod.exhaust: use explicit
(case_tac t rule: prod.exhaust) here.
+* Attributes "cases", "induct", "coinduct" support "del" option.
+
* Removed fact "case_split_thm", which duplicates "case_split".
* Command 'rep_datatype': instead of theorem names the command now