src/Provers/clasimp.ML

   val addss: Proof.context -> Proof.context
   val clarsimp_tac: Proof.context -> int -> tactic
   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
   val iff_add': attribute
   val iff_del: attribute

   end;
 
 
 (* 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 *)
 

 
 (* theory setup *)
 
 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" #>
   Method.setup @{binding auto} auto_method "auto" #>
   Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))