# HG changeset patch
# User wenzelm
# Date 1337782947 -7200
# Node ID c422128d388956469335b75a4bfe13a9adf6c952
# Parent  b8a94ed1646e8b2db896e592fb8ce3e5bc336421
discontinued obsolete method fastsimp / tactic fast_simp_tac;

diff -r b8a94ed1646e -r c422128d3889 NEWS
--- a/NEWS	Wed May 23 15:57:12 2012 +0200
+++ b/NEWS	Wed May 23 16:22:27 2012 +0200
@@ -4,6 +4,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
+is called fastforce / fast_force_tac already since Isabelle2011-1.
+
+
 
 New in Isabelle2012 (May 2012)
 ------------------------------
diff -r b8a94ed1646e -r c422128d3889 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Wed May 23 15:57:12 2012 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Wed May 23 16:22:27 2012 +0200
@@ -1094,11 +1094,11 @@
   search: it may, when backtracking from a failed proof attempt, undo
   even the step of proving a subgoal by assumption.
 
-  \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} are
-  like @{method fast}, @{method slow}, @{method best}, respectively,
-  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 fastforce}, @{method slowsimp}, @{method bestsimp}
+  are like @{method fast}, @{method slow}, @{method best},
+  respectively, but use the Simplifier as additional wrapper. The name
+  @{method fastforce}, 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 b8a94ed1646e -r c422128d3889 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Wed May 23 15:57:12 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Wed May 23 16:22:27 2012 +0200
@@ -1682,11 +1682,11 @@
   search: it may, when backtracking from a failed proof attempt, undo
   even the step of proving a subgoal by assumption.
 
-  \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. 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.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. The name
+  \hyperlink{method.fastforce}{\mbox{\isa{fastforce}}}, 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
diff -r b8a94ed1646e -r c422128d3889 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Wed May 23 15:57:12 2012 +0200
+++ b/src/Provers/clasimp.ML	Wed May 23 16:22:27 2012 +0200
@@ -173,14 +173,12 @@
 
 (* basic combinations *)
 
-fun fast_simp_tac ctxt i =
-  let val _ = legacy_feature "Old name 'fastsimp' - use 'fastforce' instead"
-  in Classical.fast_tac (addss ctxt) i end;
-
 val fast_force_tac = Classical.fast_tac o addss;
 val slow_simp_tac = Classical.slow_tac o addss;
 val best_simp_tac = Classical.best_tac o addss;
 
+
+
 (** concrete syntax **)
 
 (* attributes *)
@@ -221,7 +219,6 @@
 
 val clasimp_setup =
   Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
-  Method.setup @{binding fastsimp} (clasimp_method' fast_simp_tac) "combined fast and simp (legacy name)" #>
   Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
   Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
   Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>