1\DOC CONTR_TAC
2
3\TYPE {CONTR_TAC : thm_tactic}
4
5\SYNOPSIS
6Solves any goal from contradictory theorem.
7
8\KEYWORDS
9tactic, contradiction.
10
11\DESCRIBE
12When applied to a contradictory theorem {A' |- F}, and a goal {A ?- t},
13the tactic {CONTR_TAC} completely solves the goal. This is an invalid
14tactic unless {A'} is a subset of {A}.
15{
16    A ?- t
17   ========  CONTR_TAC (A' |- F)
18
19}
20
21
22\FAILURE
23Fails unless the theorem is contradictory, i.e. has {F} as its conclusion.
24
25\SEEALSO
26Tactic.CHECK_ASSUME_TAC, Drule.CONTR, Thm.CCONTR, Drule.CONTRAPOS, Thm.NOT_ELIM.
27\ENDDOC
28