CCONTR_TAC : tactic
STRUCTURE
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
HOL  Trindemossen-1