--- a/doc-src/IsarRef/generic.tex Tue Aug 07 16:36:52 2001 +0200
+++ b/doc-src/IsarRef/generic.tex Tue Aug 07 17:21:58 2001 +0200
@@ -843,8 +843,8 @@
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
+ declared as introduction and destruction rules. Otherwise,
+ if the rule is an inequality, the corresponding negation elimination rule
is declared, else the rule itself is declared as an introduction rule.
The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,