ASM_METIS_TAC : thm list -> tactic
Automated first-order proof search tactic using assumptions of goal.
A call to ASM_METIS_TAC[theorems] will attempt to establish the goal using
pure first-order reasoning, taking theorems and the assumptions of the goal
as the starting-point. It will usually either solve the goal completely or run
for an infeasible length of time before terminating, but it may sometimes fail
quickly. For more details, see METIS or METIS_TAC.
- FAILURE CONDITIONS
Fails if the goal is unprovable within the search bounds.
- SEE ALSO
ASM_MESON_TAC, METIS, METIS_TAC.