# HG changeset patch
# User oheimb
# Date 894054642 -7200
# Node ID 1ec740e30811e61e33dc53ffd85e457e8cb305f8
# Parent  c1aec06d1dcad838cd09c6a0df633bfc2918d7e8
Auto_tac:  now uses enhanced version of asm_full_simp_tac,
Force_tac: replaced fast_tac by best_tac

diff -r c1aec06d1dca -r 1ec740e30811 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Fri May 01 22:28:25 1998 +0200
+++ b/src/HOL/ex/Primes.ML	Fri May 01 22:30:42 1998 +0200
@@ -158,7 +158,7 @@
 
 goalw thy [prime_def] "!!p. [| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1";
 by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd_both 1);
-by (fast_tac (claset() addSss (simpset())) 1);
+by (fast_tac (claset() addss (simpset())) 1);
 qed "prime_imp_relprime";
 
 (*This theorem leads immediately to a proof of the uniqueness of factorization.
diff -r c1aec06d1dca -r 1ec740e30811 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri May 01 22:28:25 1998 +0200
+++ b/src/Provers/clasimp.ML	Fri May 01 22:30:42 1998 +0200
@@ -55,17 +55,10 @@
   fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
 end;
 
-(*an unsatisfactory fix for the incomplete safe_asm_full_simp_tac!
-  better: asm_really_full_simp_tac, a yet to be implemented version of
-			asm_full_simp_tac that applies all equalities in the
-			premises to all the premises *)
-fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
-				     safe_asm_full_simp_tac ss;
-
 (*Add a simpset to a classical set!*)
 (*Caution: only one simpset added can be added by each of addSss and addss*)
-fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
-			CHANGED o (safe_asm_more_full_simp_tac ss));
+fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
+			CHANGED o (safe_asm_full_simp_tac ss));
 fun cs addss  ss = cs addbefore  (     "asm_full_simp_tac",
 					asm_full_simp_tac ss);
 
@@ -117,7 +110,7 @@
 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),
-	ALLGOALS (fast_tac cs')]) end;
+	ALLGOALS (best_tac cs')]) end;
 fun Force_tac i = force_tac (claset(), simpset()) i;
 fun force i = by (Force_tac i);