diff -r 02cd5d5bc497 -r 57b072f00626 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Tue Aug 07 16:36:52 2001 +0200 +++ b/doc-src/IsarRef/generic.tex Tue Aug 07 17:21:58 2001 +0200 @@ -843,8 +843,8 @@ declared in several ways (depending on its structure) to the Classical Reasoner for aggressive use, which would normally be indicated by ``!''). If the rule is an equivalence, the two corresponding implications are - declared as introduction and destruction rules. Otherwise, a warning is issued - and if the rule is an inequality, the corresponding negation elimination rule + declared as introduction and destruction rules. Otherwise, + if the rule is an inequality, the corresponding negation elimination rule is declared, else the rule itself is declared as an introduction rule. The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,