1.1 --- a/doc-src/IsarRef/generic.tex	Sun Jul 22 21:31:37 2001 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Jul 23 13:50:23 2001 +0200
     1.3 @@ -837,14 +837,15 @@
     1.4    methods such as $rule$).
     1.5  \item [$rule~del$] deletes introduction, elimination, or destruction rules from
     1.6    the context.
     1.7 -\item [$iff$] declares a ``safe'' rule to the context in several ways. 
     1.8 -  The rule is declared as a rewrite rule to the Simplifier. Furthermore, it is 
     1.9 +\item [$iff$] declares a (possibly conditional) ``safe'' rule to the context in
    1.10 +  several ways.   The rule is declared as a rewrite rule to the Simplifier. 
    1.11 +  Furthermore, it is 
    1.12    declared in several ways (depending on its structure) to the Classical 
    1.13    Reasoner for aggressive use, which would normally be indicated by ``!'').
    1.14    If the rule is an equivalence, the two corresponding implications are 
    1.15    declared as introduction and destruction rules. Otherwise, a warning is issued
    1.16    and if the rule is an inequality, the corresponding negation elimination rule
    1.17 -  is declared, else the rule itself is declared as an introduction.
    1.18 +  is declared, else the rule itself is declared as an introduction rule.
    1.19    
    1.20    The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,
    1.21    and omits the Simplifier declaration.  Thus the declaration does not have