CONTR_TAC

Tactic.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 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.

See also

Tactic.CHECK_ASSUME_TAC, Drule.CONTR, Thm.CCONTR, Drule.CONTRAPOS, Thm.NOT_ELIM