diff -r abb7d0bac7e0 -r c0e62be6ef04 indrule.ML --- a/indrule.ML Thu Oct 06 09:36:40 1994 +0100 +++ b/indrule.ML Wed Oct 12 12:00:45 1994 +0100 @@ -68,8 +68,9 @@ (*Avoids backtracking by delivering the correct premise to each goal*) fun ind_tac [] 0 = all_tac - | ind_tac(prem::prems) i = REPEAT (ares_tac [Part_eqI, prem, refl] i) THEN - ind_tac prems (i-1); + | ind_tac(prem::prems) i = + DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN + ind_tac prems (i-1); val pred = Free(pred_name, elem_type --> boolT); @@ -140,15 +141,22 @@ (*Avoids backtracking by delivering the correct premise to each goal*) fun mutual_ind_tac [] 0 = all_tac | mutual_ind_tac(prem::prems) i = - SELECT_GOAL - ((*unpackage and use "prem" in the corresponding place*) - REPEAT (FIRSTGOAL - (eresolve_tac ([conjE,mp]@cmonos) ORELSE' - ares_tac [prem,impI,conjI])) - (*prove remaining goals by contradiction*) - THEN rewrite_goals_tac (con_defs@part_rec_defs) - THEN REPEAT (eresolve_tac (PartE :: sumprod_free_SEs) 1)) - i THEN mutual_ind_tac prems (i-1); + DETERM + (SELECT_GOAL + ((*unpackage and use "prem" in the corresponding place*) + REPEAT (FIRSTGOAL + (etac conjE ORELSE' eq_mp_tac ORELSE' + ares_tac [impI, conjI])) + (*prem is not allowed in the REPEAT, lest it loop!*) + THEN TRYALL (rtac prem) + THEN REPEAT + (FIRSTGOAL (ares_tac [impI] ORELSE' + eresolve_tac (mp::cmonos))) + (*prove remaining goals by contradiction*) + THEN rewrite_goals_tac (con_defs@part_rec_defs) + THEN DEPTH_SOLVE (eresolve_tac (PartE :: sumprod_free_SEs) 1)) + i) + THEN mutual_ind_tac prems (i-1); val mutual_induct_split = prove_goalw_cterm []