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