# HG changeset patch # User paulson # Date 842345287 -7200 # Node ID daa97cc96febbd9aa0e1187071906146d4853457 # Parent 0ff58b41c037cf2280b8c325b52d8fb5d71318e6 Beefed-up auto-tactic: now repeatedly simplifies if needed diff -r 0ff58b41c037 -r daa97cc96feb src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Mon Sep 09 18:58:02 1996 +0200 +++ b/src/HOL/simpdata.ML Tue Sep 10 10:48:07 1996 +0200 @@ -16,10 +16,11 @@ fun Addss ss = (claset := !claset addbefore asm_full_simp_tac ss 1); -(*Maybe swap the safe_tac and simp_tac lines?**) +(*Designed to be idempotent, except if best_tac instantiates variables + in some of the subgoals*) fun auto_tac (cs,ss) = - TRY (safe_tac cs) THEN ALLGOALS (asm_full_simp_tac ss) THEN + REPEAT (safe_tac cs THEN ALLGOALS (asm_full_simp_tac ss)) THEN REPEAT (FIRSTGOAL (best_tac (cs addss ss))); fun Auto_tac() = auto_tac (!claset, !simpset);