renamed smart_tac to force_tac, slight improvement of force_tac

--- a/src/Provers/clasimp.ML	Tue Mar 10 16:47:26 1998 +0100
+++ b/src/Provers/clasimp.ML	Tue Mar 10 18:26:27 1998 +0100
@@ -28,9 +28,9 @@
   val auto_tac	: clasimpset -> tactic
   val Auto_tac	: tactic
   val auto	: unit -> unit
-  val smart_tac	: clasimpset  -> int -> tactic
-  val Smart_tac	: int -> tactic
-  val smart	: int -> unit
+  val force_tac	: clasimpset  -> int -> tactic
+  val Force_tac	: int -> tactic
+  val force	: int -> unit
 end;
 
 structure Clasimp: CLASIMP =
@@ -114,11 +114,11 @@
 fun auto () = by Auto_tac;
 
 (* aimed to solve the given subgoal totally, using whatever tools possible *)
-fun smart_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
+fun force_tac (cs,ss) = let val cs' = cs addss ss in SELECT_GOAL (EVERY [
 	clarify_tac cs' 1,
 	IF_UNSOLVED (asm_full_simp_tac ss 1),
-	IF_UNSOLVED (fast_tac cs' 1)]) end;
-fun Smart_tac i = smart_tac (claset(), simpset()) i;
-fun smart i = by (Smart_tac i);
+	ALLGOALS (fast_tac cs')]) end;
+fun Force_tac i = force_tac (claset(), simpset()) i;
+fun force i = by (Force_tac i);
 
 end;