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