METIS_TAC : thm list -> tactic
STRUCTURE
SYNOPSIS
Performs first-order resolution to try to prove goal
DESCRIPTION
When METIS_TAC ths is applied to a goal (asl,w), it attempts to find a resolution proof that the provided theorems in ths and the assumptions in asl together imply the goal in w. METIS_TAC implements ordered resolution and as such its ability to reason about equality is generally better than MESON_TAC’s.
FAILURE
Fails if the underlying resolution machinery cannot prove the goal. METIS_TAC may also consume more and more time, and more and more memory as a search for a proof proceeds without ever explicitly failing.
COMMENTS
The alternative lower-case spelling metis_tac is also available for this tactic from the bossLib structure. There is no “metis” entrypoint that allows one to ignore the assumptions (with “meson”, there is both MESON_TAC and ASM_MESON_TAC).
SEEALSO
HOL  Kananaskis-13