doc-src/IsarRef/generic.tex
changeset 11469 57b072f00626
parent 11442 8682a88c3d6a
child 11691 fc9bd420162c
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Aug 07 16:36:52 2001 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Aug 07 17:21:58 2001 +0200
     1.3 @@ -843,8 +843,8 @@
     1.4    declared in several ways (depending on its structure) to the Classical 
     1.5    Reasoner for aggressive use, which would normally be indicated by ``!'').
     1.6    If the rule is an equivalence, the two corresponding implications are 
     1.7 -  declared as introduction and destruction rules. Otherwise, a warning is issued
     1.8 -  and if the rule is an inequality, the corresponding negation elimination rule
     1.9 +  declared as introduction and destruction rules. Otherwise, 
    1.10 +  if the rule is an inequality, the corresponding negation elimination rule
    1.11    is declared, else the rule itself is declared as an introduction rule.
    1.12    
    1.13    The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only,