1.1 --- a/src/Provers/clasimp.ML	Sat Sep 02 21:50:38 2000 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Sat Sep 02 21:51:14 2000 +0200
     1.3 @@ -45,7 +45,9 @@
     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 fast_simp_tac : clasimpset -> int -> tactic
     1.9 +  val slow_simp_tac : clasimpset -> int -> tactic
    1.10 +  val best_simp_tac : clasimpset -> int -> tactic
    1.11    val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
    1.12    val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
    1.13    val get_local_clasimpset: Proof.context -> clasimpset
    1.14 @@ -156,9 +158,13 @@
    1.15  fun force i = by (Force_tac i);
    1.16  
    1.17  
    1.18 -(* fast_simp_tac *)
    1.19 +(* basic combinations *)
    1.20  
    1.21 -fun fast_simp_tac (cs, ss) = let val cs' = cs addss ss in Classical.fast_tac cs' end;
    1.22 +fun ADDSS tac (cs, ss) = let val cs' = cs addss ss in tac cs' end;
    1.23 +
    1.24 +val fast_simp_tac = ADDSS Classical.fast_tac;
    1.25 +val slow_simp_tac = ADDSS Classical.slow_tac;
    1.26 +val best_simp_tac = ADDSS Classical.best_tac;
    1.27  
    1.28  
    1.29  (* change clasimpset *)
    1.30 @@ -212,6 +218,8 @@
    1.31  val setup =
    1.32   [Method.add_methods
    1.33     [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
    1.34 +    ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
    1.35 +    ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
    1.36      ("force", clasimp_method' force_tac, "force"),
    1.37      ("auto", auto_args auto_meth, "auto"),
    1.38      ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];