--- 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)
------------------------------
--- 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
--- 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
--- 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" #>