1\DOC CCONTR
2
3\TYPE {CCONTR : term -> thm -> thm}
4
5\SYNOPSIS
6Implements the classical contradiction rule.
7
8\KEYWORDS
9rule, contradiction.
10
11\DESCRIBE
12When applied to a term {t} and a theorem {A |- F}, the inference rule {CCONTR}
13returns the theorem {A - {~t} |- t}.
14{
15       A |- F
16   ---------------  CCONTR t
17    A - {~t} |- t
18}
19
20
21\FAILURE
22Fails unless the term has type {bool} and the theorem has {F} as its
23conclusion.
24
25\COMMENTS
26The usual use will be when {~t} exists in the assumption list; in this case,
27{CCONTR} corresponds to the classical contradiction rule: if {~t} leads to
28a contradiction, then {t} must be true.
29
30\SEEALSO
31Drule.CONTR, Drule.CONTRAPOS, Tactic.CONTR_TAC, Thm.NOT_ELIM.
32\ENDDOC
33