# HG changeset patch
# User wenzelm
# Date 1213134353 -7200
# Node ID 92e8a38fd8f69c7545c4122d8f058f9c67742b46
# Parent  9bfcdb1905e10c5dc802e8eb7cbd2768bcfeb65a
updated generated file;

diff -r 9bfcdb1905e1 -r 92e8a38fd8f6 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue Jun 10 23:45:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Tue Jun 10 23:45:53 2008 +0200
@@ -1343,7 +1343,7 @@
     'coinduct' spec
     ;
 
-    spec: ('type' | 'pred' | 'set') ':' nameref
+    spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
     ;
   \end{rail}
 
@@ -1352,12 +1352,16 @@
   \item [\hyperlink{command.print-induct-rules}{\mbox{\isa{\isacommand{print{\isacharunderscore}induct{\isacharunderscore}rules}}}}] prints cases and induct
   rules for predicates (or sets) and types of the current context.
   
-  \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{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.
+  \item [\hyperlink{attribute.cases}{\mbox{\isa{cases}}}, \hyperlink{attribute.induct}{\mbox{\isa{induct}}}, and \hyperlink{attribute.coinduct}{\mbox{\isa{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 \isa{{\isachardoublequote}del{\isachardoublequote}} specification, which
+  covers all of the \isa{{\isachardoublequote}type{\isachardoublequote}}/\isa{{\isachardoublequote}pred{\isachardoublequote}}/\isa{{\isachardoublequote}set{\isachardoublequote}}
+  sub-categories simultaneously.  For example, \hyperlink{attribute.cases}{\mbox{\isa{cases}}}~\isa{del} removes any \hyperlink{attribute.cases}{\mbox{\isa{cases}}} rules declared for
+  some type, predicate, or set.
   
   Manual rule declarations usually refer to the \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}} and \hyperlink{attribute.params}{\mbox{\isa{params}}} attributes to adjust names of
   cases and parameters of a rule; the \hyperlink{attribute.consumes}{\mbox{\isa{consumes}}}