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