835 single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not |
835 single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not |
836 applied in the search-oriented automated methods, but only in single-step |
836 applied in the search-oriented automated methods, but only in single-step |
837 methods such as $rule$). |
837 methods such as $rule$). |
838 \item [$rule~del$] deletes introduction, elimination, or destruction rules from |
838 \item [$rule~del$] deletes introduction, elimination, or destruction rules from |
839 the context. |
839 the context. |
840 \item [$iff$] declares a ``safe'' rule to the context in several ways. |
840 \item [$iff$] declares a (possibly conditional) ``safe'' rule to the context in |
841 The rule is declared as a rewrite rule to the Simplifier. Furthermore, it is |
841 several ways. The rule is declared as a rewrite rule to the Simplifier. |
|
842 Furthermore, it is |
842 declared in several ways (depending on its structure) to the Classical |
843 declared in several ways (depending on its structure) to the Classical |
843 Reasoner for aggressive use, which would normally be indicated by ``!''). |
844 Reasoner for aggressive use, which would normally be indicated by ``!''). |
844 If the rule is an equivalence, the two corresponding implications are |
845 If the rule is an equivalence, the two corresponding implications are |
845 declared as introduction and destruction rules. Otherwise, a warning is issued |
846 declared as introduction and destruction rules. Otherwise, a warning is issued |
846 and if the rule is an inequality, the corresponding negation elimination rule |
847 and if the rule is an inequality, the corresponding negation elimination rule |
847 is declared, else the rule itself is declared as an introduction. |
848 is declared, else the rule itself is declared as an introduction rule. |
848 |
849 |
849 The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, |
850 The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, |
850 and omits the Simplifier declaration. Thus the declaration does not have |
851 and omits the Simplifier declaration. Thus the declaration does not have |
851 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 |
852 $rule$ (see \S\ref{sec:misc-methods}). |
853 $rule$ (see \S\ref{sec:misc-methods}). |