# 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}}}