diff -r 54b236801671 -r 8682a88c3d6a doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sun Jul 22 21:31:37 2001 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Jul 23 13:50:23 2001 +0200
@@ -837,14 +837,15 @@
   methods such as $rule$).
 \item [$rule~del$] deletes introduction, elimination, or destruction rules from
   the context.
-\item [$iff$] declares a ``safe'' rule to the context in several ways. 
-  The rule is declared as a rewrite rule to the Simplifier. Furthermore, it is 
+\item [$iff$] declares a (possibly conditional) ``safe'' rule to the context in
+  several ways.   The rule is declared as a rewrite rule to the Simplifier. 
+  Furthermore, it is 
   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
-  is declared, else the rule itself is declared as an introduction.
+  is declared, else the rule itself is declared as an introduction rule.
   
   The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,
   and omits the Simplifier declaration.  Thus the declaration does not have