doc-src/IsarRef/generic.tex
 changeset 11442 8682a88c3d6a parent 11333 d6b69fe04c1b child 11469 57b072f00626
--- 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