CONTR_TAC : thm_tactic
Solves any goal from contradictory theorem.
When applied to a contradictory theorem
A' |- F
, and a goal
A ?- t
, the tactic
completely solves the goal. This is an invalid tactic unless
is a subset of
A ?- t ======== CONTR_TAC (A' |- F)
One quite common pattern is to use a contradictory hypothesis via
Fails unless the theorem is contradictory, i.e. has
as its conclusion.