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 Kananaskis-14