# HG changeset patch
# User nipkow
# Date 1315890829 -7200
# Node ID 884d27ede438d5143b073d99ff2330a6c0f51ac4
# Parent  53650b655b47a073010556c184d5581bd9c425cf
fastsimp -> fastforce in doc

diff -r 53650b655b47 -r 884d27ede438 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Mon Sep 12 14:49:34 2011 -0700
+++ b/doc-src/IsarRef/Thy/Generic.thy	Tue Sep 13 07:13:49 2011 +0200
@@ -933,7 +933,7 @@
     @{method_def fast} & : & @{text method} \\
     @{method_def slow} & : & @{text method} \\
     @{method_def best} & : & @{text method} \\
-    @{method_def fastsimp} & : & @{text method} \\
+    @{method_def fastforce} & : & @{text method} \\
     @{method_def slowsimp} & : & @{text method} \\
     @{method_def bestsimp} & : & @{text method} \\
     @{method_def deepen} & : & @{text method} \\
@@ -948,7 +948,7 @@
     ;
     (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * )
     ;
-    (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp})
+    (@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp})
       (@{syntax clasimpmod} * )
     ;
     @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
@@ -975,7 +975,7 @@
   \begin{itemize}
 
   \item It does not use the classical wrapper tacticals, such as the
-  integration with the Simplifier of @{method fastsimp}.
+  integration with the Simplifier of @{method fastforce}.
 
   \item It does not perform higher-order unification, as needed by the
   rule @{thm [source=false] rangeI} in HOL.  There are often
@@ -1033,9 +1033,11 @@
   search: it may, when backtracking from a failed proof attempt, undo
   even the step of proving a subgoal by assumption.
 
-  \item @{method fastsimp}, @{method slowsimp}, @{method bestsimp} are
+  \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} are
   like @{method fast}, @{method slow}, @{method best}, respectively,
-  but use the Simplifier as additional wrapper.
+  but use the Simplifier as additional wrapper. The name @{method fastforce},
+  as opposed to @{text fastsimp}, reflects the behaviour of this popular
+  method better without requiring an understanding of its implementation.
 
   \item @{method deepen} works by exhaustive search up to a certain
   depth.  The start depth is 4 (unless specified explicitly), and the
diff -r 53650b655b47 -r 884d27ede438 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon Sep 12 14:49:34 2011 -0700
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Tue Sep 13 07:13:49 2011 +0200
@@ -1379,7 +1379,7 @@
     \indexdef{}{method}{fast}\hypertarget{method.fast}{\hyperlink{method.fast}{\mbox{\isa{fast}}}} & : & \isa{method} \\
     \indexdef{}{method}{slow}\hypertarget{method.slow}{\hyperlink{method.slow}{\mbox{\isa{slow}}}} & : & \isa{method} \\
     \indexdef{}{method}{best}\hypertarget{method.best}{\hyperlink{method.best}{\mbox{\isa{best}}}} & : & \isa{method} \\
-    \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
+    \indexdef{}{method}{fastforce}\hypertarget{method.fastforce}{\hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}} & : & \isa{method} \\
     \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
     \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
     \indexdef{}{method}{deepen}\hypertarget{method.deepen}{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}} & : & \isa{method} \\
@@ -1431,7 +1431,7 @@
 \rail@end
 \rail@begin{3}{}
 \rail@bar
-\rail@term{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}}[]
+\rail@term{\hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}}[]
 \rail@nextbar{1}
 \rail@term{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}}[]
 \rail@nextbar{2}
@@ -1549,7 +1549,7 @@
   \begin{itemize}
 
   \item It does not use the classical wrapper tacticals, such as the
-  integration with the Simplifier of \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}.
+  integration with the Simplifier of \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}.
 
   \item It does not perform higher-order unification, as needed by the
   rule \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f} in HOL.  There are often
@@ -1605,9 +1605,11 @@
   search: it may, when backtracking from a failed proof attempt, undo
   even the step of proving a subgoal by assumption.
 
-  \item \hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are
+  \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are
   like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
-  but use the Simplifier as additional wrapper.
+  but use the Simplifier as additional wrapper. The name \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}},
+  as opposed to \isa{fastsimp}, reflects the behaviour of this popular
+  method better without requiring an understanding of its implementation.
 
   \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
   depth.  The start depth is 4 (unless specified explicitly), and the