----------------------------------------------------------------------
CONTR                                                          (Drule)
----------------------------------------------------------------------
CONTR : term -> thm -> thm

SYNOPSIS
Implements the intuitionistic contradiction rule.

KEYWORDS
rule, contradiction.

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

    A |- F
   --------  CONTR t
    A |- t




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

SEEALSO
Thm.CCONTR, Drule.CONTRAPOS, Tactic.CONTR_TAC, Thm.NOT_ELIM.

----------------------------------------------------------------------