841 several ways. The rule is declared as a rewrite rule to the Simplifier. |
841 several ways. The rule is declared as a rewrite rule to the Simplifier. |
842 Furthermore, it is |
842 Furthermore, it is |
843 declared in several ways (depending on its structure) to the Classical |
843 declared in several ways (depending on its structure) to the Classical |
844 Reasoner for aggressive use, which would normally be indicated by ``!''). |
844 Reasoner for aggressive use, which would normally be indicated by ``!''). |
845 If the rule is an equivalence, the two corresponding implications are |
845 If the rule is an equivalence, the two corresponding implications are |
846 declared as introduction and destruction rules. Otherwise, a warning is issued |
846 declared as introduction and destruction rules. Otherwise, |
847 and if the rule is an inequality, the corresponding negation elimination rule |
847 if the rule is an inequality, the corresponding negation elimination rule |
848 is declared, else the rule itself is declared as an introduction rule. |
848 is declared, else the rule itself is declared as an introduction rule. |
849 |
849 |
850 The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, |
850 The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, |
851 and omits the Simplifier declaration. Thus the declaration does not have |
851 and omits the Simplifier declaration. Thus the declaration does not have |
852 any effect on automated proof tools, but only on simple methods such as |
852 any effect on automated proof tools, but only on simple methods such as |