1.1 --- a/NEWS	Wed May 23 15:57:12 2012 +0200
     1.2 +++ b/NEWS	Wed May 23 16:22:27 2012 +0200
     1.3 @@ -4,6 +4,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
    1.10 +is called fastforce / fast_force_tac already since Isabelle2011-1.
    1.11 +
    1.12 +
    1.13  
    1.14  New in Isabelle2012 (May 2012)
    1.15  ------------------------------

     2.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Wed May 23 15:57:12 2012 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Wed May 23 16:22:27 2012 +0200
     2.3 @@ -1094,11 +1094,11 @@
     2.4    search: it may, when backtracking from a failed proof attempt, undo
     2.5    even the step of proving a subgoal by assumption.
     2.6  
     2.7 -  \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} are
     2.8 -  like @{method fast}, @{method slow}, @{method best}, respectively,
     2.9 -  but use the Simplifier as additional wrapper. The name @{method fastforce},
    2.10 -  as opposed to @{text fastsimp}, reflects the behaviour of this popular
    2.11 -  method better without requiring an understanding of its implementation.
    2.12 +  \item @{method fastforce}, @{method slowsimp}, @{method bestsimp}
    2.13 +  are like @{method fast}, @{method slow}, @{method best},
    2.14 +  respectively, but use the Simplifier as additional wrapper. The name
    2.15 +  @{method fastforce}, reflects the behaviour of this popular method
    2.16 +  better without requiring an understanding of its implementation.
    2.17  
    2.18    \item @{method deepen} works by exhaustive search up to a certain
    2.19    depth.  The start depth is 4 (unless specified explicitly), and the

     3.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Wed May 23 15:57:12 2012 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Wed May 23 16:22:27 2012 +0200
     3.3 @@ -1682,11 +1682,11 @@
     3.4    search: it may, when backtracking from a failed proof attempt, undo
     3.5    even the step of proving a subgoal by assumption.
     3.6  
     3.7 -  \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}} are
     3.8 -  like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
     3.9 -  but use the Simplifier as additional wrapper. The name \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}},
    3.10 -  as opposed to \isa{fastsimp}, reflects the behaviour of this popular
    3.11 -  method better without requiring an understanding of its implementation.
    3.12 +  \item \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, \hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}, \hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}
    3.13 +  are like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}},
    3.14 +  respectively, but use the Simplifier as additional wrapper. The name
    3.15 +  \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, reflects the behaviour of this popular method
    3.16 +  better without requiring an understanding of its implementation.
    3.17  
    3.18    \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
    3.19    depth.  The start depth is 4 (unless specified explicitly), and the

     4.1 --- a/src/Provers/clasimp.ML	Wed May 23 15:57:12 2012 +0200
     4.2 +++ b/src/Provers/clasimp.ML	Wed May 23 16:22:27 2012 +0200
     4.3 @@ -173,14 +173,12 @@
     4.4  
     4.5  (* basic combinations *)
     4.6  
     4.7 -fun fast_simp_tac ctxt i =
     4.8 -  let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead"
     4.9 -  in Classical.fast_tac (addss ctxt) i end;
    4.10 -
    4.11  val fast_force_tac = Classical.fast_tac o addss;
    4.12  val slow_simp_tac = Classical.slow_tac o addss;
    4.13  val best_simp_tac = Classical.best_tac o addss;
    4.14  
    4.15 +
    4.16 +
    4.17  (** concrete syntax **)
    4.18  
    4.19  (* attributes *)
    4.20 @@ -221,7 +219,6 @@
    4.21  
    4.22  val clasimp_setup =
    4.23    Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
    4.24 -  Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #>
    4.25    Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
    4.26    Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
    4.27    Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>