1.1 --- a/src/Provers/clasimp.ML	Mon Aug 14 14:51:51 2000 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Mon Aug 14 14:53:26 2000 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4    val force_tac	  : clasimpset  -> int -> tactic
     1.5    val Force_tac	  : int -> tactic
     1.6    val force	  : int -> unit
     1.7 +  val fast_simp_tac : clasimpset  -> int -> tactic
     1.8    val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
     1.9    val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
    1.10    val get_local_clasimpset: Proof.context -> clasimpset
    1.11 @@ -154,6 +155,11 @@
    1.12  fun force i = by (Force_tac i);
    1.13  
    1.14  
    1.15 +(* fast_simp_tac *)
    1.16 +
    1.17 +fun fast_simp_tac (cs, ss) = let val cs' = cs addss ss in Classical.fast_tac cs' end;
    1.18 +
    1.19 +
    1.20  (* attributes *)
    1.21  
    1.22  fun change_global_css f (thy, th) =
    1.23 @@ -195,9 +201,10 @@
    1.24  
    1.25  val setup =
    1.26   [Method.add_methods
    1.27 -   [("force", clasimp_method' force_tac, "force"),
    1.28 +   [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
    1.29 +    ("force", clasimp_method' force_tac, "force"),
    1.30      ("auto", clasimp_method (CHANGED o auto_tac), "auto"),
    1.31 -    ("clarsimp", clasimp_method' clarsimp_tac, "clarify simplified goal")]];
    1.32 +    ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
    1.33  
    1.34  
    1.35  end;