doc-src/IsarRef/generic.tex
changeset 8594 d2e2a3df6871
parent 8547 93b8685d004b
child 8619 63a0e1502e41
equal deleted inserted replaced
8593:68619606c5d1 8594:d2e2a3df6871
   363   ;
   363   ;
   364 \end{rail}
   364 \end{rail}
   365 
   365 
   366 \begin{descr}
   366 \begin{descr}
   367 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
   367 \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
   368   according to the arguments given.  Note that the \railtoken{only} modifier
   368   according to the arguments given.  Note that the \railtterm{only} modifier
   369   first removes all other rewrite rules, congruences, and looper tactics
   369   first removes all other rewrite rules, congruences, and looper tactics
   370   (including splits), and then behaves like \railtoken{add}.
   370   (including splits), and then behaves like \railtterm{add}.
   371   
   371   
   372   The \railtoken{split} modifiers add or delete rules for the Splitter (see
   372   The \railtterm{split} modifiers add or delete rules for the Splitter (see
   373   also \cite{isabelle-ref}), the default is to add.  This works only if the
   373   also \cite{isabelle-ref}), the default is to add.  This works only if the
   374   Simplifier method has been properly setup to include the Splitter (all major
   374   Simplifier method has been properly setup to include the Splitter (all major
   375   object logics such HOL, HOLCF, FOL, ZF do this already).
   375   object logics such HOL, HOLCF, FOL, ZF do this already).
   376   
   376   
   377   The \railtoken{other} modifier ignores its arguments.  Nevertheless,
   377   The \railtterm{other} modifier ignores its arguments.  Nevertheless,
   378   additional kinds of rules may be declared by including appropriate
   378   additional kinds of rules may be declared by including appropriate
   379   attributes in the specification.
   379   attributes in the specification.
   380 \item [$simp_all$] is similar to $simp$, but acts on all goals.
   380 \item [$simp_all$] is similar to $simp$, but acts on all goals.
   381 \end{descr}
   381 \end{descr}
   382 
   382 
   534 \item [$force$ and $auto$] provide access to Isabelle's combined
   534 \item [$force$ and $auto$] provide access to Isabelle's combined
   535   simplification and classical reasoning tactics.  See \texttt{force_tac} and
   535   simplification and classical reasoning tactics.  See \texttt{force_tac} and
   536   \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
   536   \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
   537   modifier arguments correspond to those given in \S\ref{sec:simp} and
   537   modifier arguments correspond to those given in \S\ref{sec:simp} and
   538   \S\ref{sec:classical-auto}.  Just note that the ones related to the
   538   \S\ref{sec:classical-auto}.  Just note that the ones related to the
   539   Simplifier are prefixed by \railtoken{simp} here.
   539   Simplifier are prefixed by \railtterm{simp} here.
   540   
   540   
   541   Facts provided by forward chaining are inserted into the goal before doing
   541   Facts provided by forward chaining are inserted into the goal before doing
   542   the search.  The ``!''~argument causes the full context of assumptions to be
   542   the search.  The ``!''~argument causes the full context of assumptions to be
   543   included as well.
   543   included as well.
   544 \end{descr}
   544 \end{descr}