doc-src/IsarRef/generic.tex
changeset 11442 8682a88c3d6a
parent 11333 d6b69fe04c1b
child 11469 57b072f00626
equal deleted inserted replaced
11441:54b236801671 11442:8682a88c3d6a
   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}).