CCONTR_TAC : tactic
STRUCTURE
Tactic
SYNOPSIS
Prepares for a proof by Classical contradiction.
DESCRIPTION
CCONTR_TAC
takes a theorem
A' |- F
and completely solves the goal. This is an invalid tactic unless
A'
is a subset of
A
.
A ?- t ======== CCONTR_TAC (A' |- F)
FAILURE
Fails unless the theorem is contradictory, i.e. has
F
as its conclusion.
SEEALSO
CHECK_ASSUME_TAC
,
CCONTR
,
CONTRAPOS
,
NOT_ELIM
HOL
Kananaskis-11