CCONTR_TAC

Tactic.CCONTR_TAC : tactic

Assumes the negation of the conclusion of a goal.

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

See also

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