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