CCONTR_TAC : tactic
STRUCTURE
Tactic
SYNOPSIS
Assumes the negation of the conclusion of a goal.
DESCRIPTION
Given a goal A ?- t, CCONTR_TAC makes a new goal which is to prove F by assuming also the negation of the conclusion t. 
     A ?- t
   ==========
   A, -t ?- F

FAILURE
Never fails
SEEALSO
CHECK_ASSUME_TAC, CCONTR, CONTRAPOS, NOT_ELIM
HOL  Trindemossen-1