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  Trindemossen-1