CCONTR : term -> thm -> thm
- SYNOPSIS
-
Implements the classical contradiction rule.
- DESCRIPTION
-
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 CONDITIONS
-
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.
- SEE ALSO
-
CONTR, CONTR_TAC, NOT_ELIM.