# HG changeset patch
# User wenzelm
# Date 966257606 -7200
# Node ID 590d36e059d164f5669c073fa4aae2f2123c1242
# Parent  52e71612e42f54a47e5a6c737d8dc6b0d5aa3257
added "fastsimp";
fixed "clarsimp": CHANGED;

diff -r 52e71612e42f -r 590d36e059d1 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Mon Aug 14 14:51:51 2000 +0200
+++ b/src/Provers/clasimp.ML	Mon Aug 14 14:53:26 2000 +0200
@@ -45,6 +45,7 @@
   val force_tac	  : clasimpset  -> int -> tactic
   val Force_tac	  : int -> tactic
   val force	  : int -> unit
+  val fast_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
@@ -154,6 +155,11 @@
 fun force i = by (Force_tac i);
 
 
+(* fast_simp_tac *)
+
+fun fast_simp_tac (cs, ss) = let val cs' = cs addss ss in Classical.fast_tac cs' end;
+
+
 (* attributes *)
 
 fun change_global_css f (thy, th) =
@@ -195,9 +201,10 @@
 
 val setup =
  [Method.add_methods
-   [("force", clasimp_method' force_tac, "force"),
+   [("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
+    ("force", clasimp_method' force_tac, "force"),
     ("auto", clasimp_method (CHANGED o auto_tac), "auto"),
-    ("clarsimp", clasimp_method' clarsimp_tac, "clarify simplified goal")]];
+    ("clarsimp", clasimp_method' (CHANGED oo clarsimp_tac), "clarify simplified goal")]];
 
 
 end;