181 REPEAT_DETERM_N k (eresolve_tac [thin_rl] 1 THEN rotate_tac 1 1), |
181 REPEAT_DETERM_N k (eresolve_tac [thin_rl] 1 THEN rotate_tac 1 1), |
182 eresolve_tac [elim] 1, |
182 eresolve_tac [elim] 1, |
183 REPEAT_DETERM_N j distinct_tac, |
183 REPEAT_DETERM_N j distinct_tac, |
184 TRY (dresolve_tac inject 1), |
184 TRY (dresolve_tac inject 1), |
185 REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1, |
185 REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1, |
186 REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]), |
186 REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac ctxt 1]), |
187 TRY (hyp_subst_tac ctxt 1), |
187 TRY (hyp_subst_tac ctxt 1), |
188 resolve_tac [refl] 1, |
188 resolve_tac [refl] 1, |
189 REPEAT_DETERM_N (n - j - 1) distinct_tac], |
189 REPEAT_DETERM_N (n - j - 1) distinct_tac], |
190 intrs, j + 1) |
190 intrs, j + 1) |
191 end; |
191 end; |