1\DOC CCONTR_TAC
2
3\TYPE {CCONTR_TAC : tactic}
4
5\SYNOPSIS
6Assumes the negation of the conclusion of a goal.
7
8\KEYWORDS
9tactic, contradiction.
10
11\DESCRIBE
12Given a goal {A ?- t}, {CCONTR_TAC} makes a new goal which is to prove {F}
13by assuming also the negation of the conclusion {t}.
14{
15     A ?- t
16   ==========
17   A, -t ?- F
18}
19
20
21\FAILURE
22Never fails
23
24\SEEALSO
25Tactic.CHECK_ASSUME_TAC, Thm.CCONTR, Drule.CONTRAPOS, Thm.NOT_ELIM.
26
27\ENDDOC
28