CCONTR_TAC : tactic
STRUCTURE
SYNOPSIS
Prepares for a proof by Classical contradiction.
DESCRIPTION
CCONTR_TAC takes a theorem A' |- F and completely solves the goal. This is an invalid tactic unless A' is a subset of A.
    A ?- t
   ========  CCONTR_TAC (A' |- F)

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