diff -r 11ab8c8ce694 -r d6b69fe04c1b doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed May 30 18:54:10 2001 +0200
+++ b/doc-src/IsarRef/generic.tex	Thu May 31 12:43:56 2001 +0200
@@ -842,9 +842,9 @@
   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. If it is an inequality, the
-  corresponding elimination rule is declared. Otherwise, a warning is issued
-  and the rule is delcared as an intruction.
+  declared as introduction and destruction rules. Otherwise, a warning is issued
+  and if the rule is an inequality, the corresponding negation elimination rule
+  is declared, else the rule itself is declared as an introduction.
   
   The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,
   and omits the Simplifier declaration.  Thus the declaration does not have