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