# HG changeset patch
# User wenzelm
# Date 964476759 -7200
# Node ID 6131037f8a1158c7d7f77cc1ee01a2f49d43c8f1
# Parent  93e91040c286568ba6a3ae03c1856efe1f839638
removed slow, slow_best methods;
added clarify, clarsimp methods;

diff -r 93e91040c286 -r 6131037f8a11 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Tue Jul 25 00:11:38 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Tue Jul 25 00:12:39 2000 +0200
@@ -531,23 +531,18 @@
 
 \subsection{Automated methods}\label{sec:classical-auto}
 
-\indexisarmeth{blast}
-\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
+\indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{clarify}
 \begin{matharray}{rcl}
  blast & : & \isarmeth \\
  fast & : & \isarmeth \\
  best & : & \isarmeth \\
- slow & : & \isarmeth \\
- slow_best & : & \isarmeth \\
+ clarify & : & \isarmeth \\
 \end{matharray}
 
-\railalias{slowbest}{slow\_best}
-\railterm{slowbest}
-
 \begin{rail}
   'blast' ('!' ?) nat? (clamod * )
   ;
-  ('fast' | 'best' | 'slow' | slowbest) ('!' ?) (clamod * )
+  ('fast' | 'best' | 'clarify') ('!' ?) (clamod * )
   ;
 
   clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
@@ -558,8 +553,9 @@
 \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   user-supplied search bound (default 20).
-\item [$fast$, $best$, $slow$, $slow_best$] refer to the generic classical
-  reasoner (see \cite[\S11]{isabelle-ref}, tactic \texttt{fast_tac} etc).
+\item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner.
+  See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in
+  \cite[\S11]{isabelle-ref} for more information.
 \end{descr}
 
 Any of above methods support additional modifiers of the context of classical
@@ -574,14 +570,15 @@
 
 \subsection{Combined automated methods}
 
-\indexisarmeth{auto}\indexisarmeth{force}
+\indexisarmeth{force}\indexisarmeth{auto}\indexisarmeth{clarsimp}
 \begin{matharray}{rcl}
   force & : & \isarmeth \\
   auto & : & \isarmeth \\
+  clarsimp & : & \isarmeth \\
 \end{matharray}
 
 \begin{rail}
-  ('force' | 'auto') ('!' ?) (clasimpmod * )
+  ('force' | 'auto' | 'clarsimp') ('!' ?) (clasimpmod * )
   ;
 
   clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
@@ -590,12 +587,12 @@
 \end{rail}
 
 \begin{descr}
-\item [$force$ and $auto$] provide access to Isabelle's combined
-  simplification and classical reasoning tactics.  See \texttt{force_tac} and
-  \texttt{auto_tac} in \cite[\S11]{isabelle-ref} for more information.  The
-  modifier arguments correspond to those given in \S\ref{sec:simp} and
-  \S\ref{sec:classical-auto}.  Just note that the ones related to the
-  Simplifier are prefixed by \railtterm{simp} here.
+\item [$force$, $auto$, and $clarsimp$] provide access to Isabelle's combined
+  simplification and classical reasoning tactics.  See \texttt{force_tac},
+  \texttt{auto_tac}, and \texttt{clarsimp_tac} in \cite[\S11]{isabelle-ref}
+  for more information.  The modifier arguments correspond to those given in
+  \S\ref{sec:simp} and \S\ref{sec:classical-auto}.  Just note that the ones
+  related to the Simplifier are prefixed by \railtterm{simp} here.
   
   Facts provided by forward chaining are inserted into the goal before doing
   the search.  The ``!''~argument causes the full context of assumptions to be