equal
deleted
inserted
replaced
144 val main_tac = |
144 val main_tac = |
145 Blast.depth_tac ctxt m (* fast but can't use wrappers *) |
145 Blast.depth_tac ctxt m (* fast but can't use wrappers *) |
146 ORELSE' |
146 ORELSE' |
147 (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) |
147 (CHANGED o nodup_depth_tac (addss ctxt) n); (* slower but more general *) |
148 in |
148 in |
149 PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ctxt)) THEN |
149 PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN |
150 TRY (Classical.safe_tac ctxt) THEN |
150 TRY (Classical.safe_tac ctxt) THEN |
151 REPEAT_DETERM (FIRSTGOAL main_tac) THEN |
151 REPEAT_DETERM (FIRSTGOAL main_tac) THEN |
152 TRY (Classical.safe_tac (addSss ctxt)) THEN |
152 TRY (Classical.safe_tac (addSss ctxt)) THEN |
153 prune_params_tac ctxt |
153 prune_params_tac ctxt |
154 end; |
154 end; |