1\DOC 2 3\TYPE {METIS_TAC : thm list -> tactic} 4 5\SYNOPSIS 6Performs first-order resolution to try to prove goal 7 8\KEYWORDS 9Tactic, resolution. 10 11\DESCRIBE 12When {METIS_TAC ths} is applied to a goal {(asl,w)}, it attempts to 13find a resolution proof that the provided theorems in {ths} and the 14assumptions in {asl} together imply the goal in {w}. {METIS_TAC} 15implements ordered resolution and as such its ability to reason about 16equality is generally better than {MESON_TAC}'s. 17 18\FAILURE 19Fails if the underlying resolution machinery cannot prove the goal. 20{METIS_TAC} may also consume more and more time, and more and more 21memory as a search for a proof proceeds without ever explicitly 22failing. 23 24\COMMENTS 25The alternative lower-case spelling {metis_tac} is also available for 26this tactic from the {bossLib} structure. There is no ``metis'' 27entrypoint that allows one to ignore the assumptions (with ``meson'', 28there is both {MESON_TAC} and {ASM_MESON_TAC}). 29 30\SEEALSO 31mesonLib.MESON_TAC. 32 33\ENDDOC 34