--- a/src/Provers/clasimp.ML Sun Sep 11 22:56:05 2011 +0200
+++ b/src/Provers/clasimp.ML Mon Sep 12 07:55:43 2011 +0200
@@ -23,7 +23,7 @@
val mk_auto_tac: Proof.context -> int -> int -> tactic
val auto_tac: Proof.context -> tactic
val force_tac: Proof.context -> int -> tactic
- val fast_simp_tac: Proof.context -> int -> tactic
+ val fast_force_tac: Proof.context -> int -> tactic
val slow_simp_tac: Proof.context -> int -> tactic
val best_simp_tac: Proof.context -> int -> tactic
val iff_add: attribute
@@ -169,12 +169,14 @@
(* basic combinations *)
-val fast_simp_tac = Classical.fast_tac o addss;
+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 *)
@@ -215,7 +217,8 @@
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" #>
+ 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" #>
Method.setup @{binding force} (clasimp_method' force_tac) "force" #>