1\DOC CHECK_ASSUME_TAC
2
3\TYPE {CHECK_ASSUME_TAC : thm_tactic}
4
5\SYNOPSIS
6Adds a theorem to the assumption list of goal, unless it solves the goal.
7
8\KEYWORDS
9tactic, assumption.
10
11\DESCRIBE
12When applied to a theorem {A' |- s} and a goal {A ?- t}, the tactic
13{CHECK_ASSUME_TAC} checks whether the theorem will solve the goal (this
14includes the possibility that the theorem is just {A' |- F}). If so, the goal
15is duly solved. If not, the theorem is added to the assumptions of the goal,
16unless it is already there.
17{
18       A ?- t
19   ==============  CHECK_ASSUME_TAC (A' |- F)   [special case 1]
20
21
22       A ?- t
23   ==============  CHECK_ASSUME_TAC (A' |- t)   [special case 2]
24
25
26       A ?- t
27   ==============  CHECK_ASSUME_TAC (A' |- s)   [general case]
28    A u {s} ?- t
29}
30Unless {A'} is a subset of {A}, the tactic will be invalid, although
31it will not fail.
32
33\FAILURE
34Never fails.
35
36\SEEALSO
37Tactic.ACCEPT_TAC, Tactic.ASSUME_TAC, Tactic.CONTR_TAC, Tactic.DISCARD_TAC, Tactic.MATCH_ACCEPT_TAC.
38\ENDDOC
39