CONTR_TAC : thm_tactic

- STRUCTURE
- SYNOPSIS
- Solves any goal from contradictory theorem.
- DESCRIPTION
- When applied to a contradictory theorem A' |- F, and a goal A ?- t, the tactic CONTR_TAC completely solves the goal. This is an invalid tactic unless A' is a subset of A.
A ?- t ======== CONTR_TAC (A' |- F)

- FAILURE
- Fails unless the theorem is contradictory, i.e. has F as its conclusion.
- SEEALSO

HOL Kananaskis-14