CHECK_ASSUME_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Adds a theorem to the assumption list of goal, unless it solves the goal.
- DESCRIPTION
- When applied to a theorem A' |- s and a goal A ?- t, the tactic CHECK_ASSUME_TAC checks whether the theorem will solve the goal (this includes the possibility that the theorem is just A' |- F). If so, the goal is duly solved. If not, the theorem is added to the assumptions of the goal, unless it is already there.Unless A' is a subset of A, the tactic will be invalid, although it will not fail.
A ?- t ============== CHECK_ASSUME_TAC (A' |- F) [special case 1] A ?- t ============== CHECK_ASSUME_TAC (A' |- t) [special case 2] A ?- t ============== CHECK_ASSUME_TAC (A' |- s) [general case] A u {s} ?- t

- FAILURE
- Never fails.
- SEEALSO

HOL Kananaskis-14