\DOC CCONTR

\TYPE {CCONTR : term -> thm -> thm}

\SYNOPSIS
Implements the classical contradiction rule.

\KEYWORDS
rule, contradiction.

\DESCRIBE
When applied to a term {t} and a theorem {A |- F}, the inference rule {CCONTR}
returns the theorem {A - {~t} |- t}.
{
       A |- F
   ---------------  CCONTR t
    A - {~t} |- t
}


\FAILURE
Fails unless the term has type {bool} and the theorem has {F} as its
conclusion.

\COMMENTS
The usual use will be when {~t} exists in the assumption list; in this case,
{CCONTR} corresponds to the classical contradiction rule: if {~t} leads to
a contradiction, then {t} must be true.

\SEEALSO
Drule.CONTR, Drule.CONTRAPOS, Tactic.CONTR_TAC, Thm.NOT_ELIM.
\ENDDOC