# HG changeset patch
# User wenzelm
# Date 967924274 -7200
# Node ID 10b617bdd02883da39777d681b27c6703d4b09ca
# Parent  ee0c337327cf6b2b7c7400c1d9b25a131b3f0a75
added "slowsimp", "bestsimp";

diff -r ee0c337327cf -r 10b617bdd028 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Sep 02 21:50:38 2000 +0200
+++ b/src/Provers/clasimp.ML	Sat Sep 02 21:51:14 2000 +0200
@@ -45,7 +45,9 @@
   val force_tac   : clasimpset  -> int -> tactic
   val Force_tac   : int -> tactic
   val force       : int -> unit
-  val fast_simp_tac : clasimpset  -> int -> tactic
+  val fast_simp_tac : clasimpset -> int -> tactic
+  val slow_simp_tac : clasimpset -> int -> tactic
+  val best_simp_tac : clasimpset -> int -> tactic
   val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
   val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
   val get_local_clasimpset: Proof.context -> clasimpset
@@ -156,9 +158,13 @@
 fun force i = by (Force_tac i);
 
 
-(* fast_simp_tac *)
+(* basic combinations *)
+
+fun ADDSS tac (cs, ss) = let val cs' = cs addss ss in tac cs' end;
 
-fun fast_simp_tac (cs, ss) = let val cs' = cs addss ss in Classical.fast_tac cs' end;
+val fast_simp_tac = ADDSS Classical.fast_tac;
+val slow_simp_tac = ADDSS Classical.slow_tac;
+val best_simp_tac = ADDSS Classical.best_tac;
 
 
 (* change clasimpset *)
@@ -212,6 +218,8 @@
 val setup =
  [Method.add_methods
    [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
+    ("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
+    ("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
     ("force", clasimp_method' force_tac, "force"),
     ("auto", auto_args auto_meth, "auto"),
     ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];