DISCARD_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Discards a theorem already present in a goal’s assumptions.
- DESCRIPTION
- When applied to a theorem A' |- s and a goal, DISCARD_TAC checks that s is simply T (true), or already exists (up to alpha-conversion) in the assumption list of the goal. In either case, the tactic has no effect. Otherwise, it fails.
A ?- t ======== DISCARD_TAC (A' |- s) A ?- t

- FAILURE
- Fails if the above conditions are not met, i.e. the theorem’s conclusion is not T or already in the assumption list (up to alpha-conversion).
- SEEALSO

HOL Kananaskis-14