# HG changeset patch
# User oheimb
# Date 997197718 -7200
# Node ID 57b072f00626c770a48070f194ccbfec9f1bba48
# Parent  02cd5d5bc4974207dc4476b0e0a7f5e6f396117f
removed the warning from [iff]

diff -r 02cd5d5bc497 -r 57b072f00626 doc-src/IsarRef/generic.tex
--- 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,