# HG changeset patch
# User wenzelm
# Date 1213134351 -7200
# Node ID 9bfcdb1905e10c5dc802e8eb7cbd2768bcfeb65a
# Parent  327a73f02d5fba7174a1a564dadb916218219dbf
* Attributes cases, induct, coinduct support del option.

diff -r 327a73f02d5f -r 9bfcdb1905e1 NEWS
--- 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
diff -r 327a73f02d5f -r 9bfcdb1905e1 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Tue Jun 10 23:28:42 2008 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Tue Jun 10 23:45:51 2008 +0200
@@ -1372,7 +1372,7 @@
     'coinduct' spec
     ;
 
-    spec: ('type' | 'pred' | 'set') ':' nameref
+    spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
     ;
   \end{rail}
 
@@ -1382,12 +1382,17 @@
   rules for predicates (or sets) and types of the current context.
   
   \item [@{attribute cases}, @{attribute induct}, and @{attribute
-  coinduct}] (as attributes) augment the corresponding context of
-  rules for reasoning about (co)inductive predicates (or sets) and
-  types, using the corresponding methods of the same name.  Certain
-  definitional packages of object-logics usually declare emerging
-  cases and induction rules as expected, so users rarely need to
-  intervene.
+  coinduct}] (as attributes) declare rules for reasoning about
+  (co)inductive predicates (or sets) and types, using the
+  corresponding methods of the same name.  Certain definitional
+  packages of object-logics usually declare emerging cases and
+  induction rules as expected, so users rarely need to intervene.
+
+  Rules may be deleted via the @{text "del"} specification, which
+  covers all of the @{text "type"}/@{text "pred"}/@{text "set"}
+  sub-categories simultaneously.  For example, @{attribute
+  cases}~@{text del} removes any @{attribute cases} rules declared for
+  some type, predicate, or set.
   
   Manual rule declarations usually refer to the @{attribute
   case_names} and @{attribute params} attributes to adjust names of