--- 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