doc-src/IsarRef/generic.tex
changeset 9438 6131037f8a11
parent 9408 d3d56e1d2ec1
child 9480 7afb808b6b3e
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Jul 25 00:11:38 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Jul 25 00:12:39 2000 +0200
     1.3 @@ -531,23 +531,18 @@
     1.4  
     1.5  \subsection{Automated methods}\label{sec:classical-auto}
     1.6  
     1.7 -\indexisarmeth{blast}
     1.8 -\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
     1.9 +\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{clarify}
    1.10  \begin{matharray}{rcl}
    1.11   blast & : & \isarmeth \\
    1.12   fast & : & \isarmeth \\
    1.13   best & : & \isarmeth \\
    1.14 - slow & : & \isarmeth \\
    1.15 - slow_best & : & \isarmeth \\
    1.16 + clarify & : & \isarmeth \\
    1.17  \end{matharray}
    1.18  
    1.19 -\railalias{slowbest}{slow\_best}
    1.20 -\railterm{slowbest}
    1.21 -
    1.22  \begin{rail}
    1.23    'blast' ('!' ?) nat? (clamod * )
    1.24    ;
    1.25 -  ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
    1.26 +  ('fast' | 'best' | 'clarify') ('!' ?) (clamod * )
    1.27    ;
    1.28  
    1.29    clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
    1.30 @@ -558,8 +553,9 @@
    1.31  \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
    1.32    in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
    1.33    user-supplied search bound (default 20).
    1.34 -\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
    1.35 -  reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
    1.36 +\item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner.
    1.37 +  See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in
    1.38 +  \cite[\S11]{isabelle-ref} for more information.
    1.39  \end{descr}
    1.40  
    1.41  Any of above methods support additional modifiers of the context of classical
    1.42 @@ -574,14 +570,15 @@
    1.43  
    1.44  \subsection{Combined automated methods}
    1.45  
    1.46 -\indexisarmeth{auto}\indexisarmeth{force}
    1.47 +\indexisarmeth{force}\indexisarmeth{auto}\indexisarmeth{clarsimp}
    1.48  \begin{matharray}{rcl}
    1.49    force & : & \isarmeth \\
    1.50    auto & : & \isarmeth \\
    1.51 +  clarsimp & : & \isarmeth \\
    1.52  \end{matharray}
    1.53  
    1.54  \begin{rail}
    1.55 -  ('force' | 'auto') ('!' ?) (clasimpmod * )
    1.56 +  ('force' | 'auto' | 'clarsimp') ('!' ?) (clasimpmod * )
    1.57    ;
    1.58  
    1.59    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
    1.60 @@ -590,12 +587,12 @@
    1.61  \end{rail}
    1.62  
    1.63  \begin{descr}
    1.64 -\item [$force$ and $auto$] provide access to Isabelle's combined
    1.65 -  simplification and classical reasoning tactics.  See \texttt{force_tac} and
    1.66 -  \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
    1.67 -  modifier arguments correspond to those given in \S\ref{sec:simp} and
    1.68 -  \S\ref{sec:classical-auto}.  Just note that the ones related to the
    1.69 -  Simplifier are prefixed by \railtterm{simp} here.
    1.70 +\item [$force$, $auto$, and $clarsimp$] provide access to Isabelle's combined
    1.71 +  simplification and classical reasoning tactics.  See \texttt{force_tac},
    1.72 +  \texttt{auto_tac}, and \texttt{clarsimp_tac} in \cite[\S11]{isabelle-ref}
    1.73 +  for more information.  The modifier arguments correspond to those given in
    1.74 +  \S\ref{sec:simp} and \S\ref{sec:classical-auto}.  Just note that the ones
    1.75 +  related to the Simplifier are prefixed by \railtterm{simp} here.
    1.76    
    1.77    Facts provided by forward chaining are inserted into the goal before doing
    1.78    the search.  The ``!''~argument causes the full context of assumptions to be