1\DOC EQ_TAC 2 3\TYPE {EQ_TAC : tactic} 4 5\SYNOPSIS 6Reduces goal of equality of boolean terms to forward and backward implication. 7 8\KEYWORDS 9tactic, equality, implication. 10 11\DESCRIBE 12When applied to a goal {A ?- t1 = t2}, where {t1} and {t2} have type {bool}, 13the tactic {EQ_TAC} returns the subgoals {A ?- t1 ==> t2} and 14{A ?- t2 ==> t1}. 15{ 16 A ?- t1 = t2 17 ================================= EQ_TAC 18 A ?- t1 ==> t2 A ?- t2 ==> t1 19} 20 21 22\FAILURE 23Fails unless the conclusion of the goal is an equation between boolean terms. 24 25\SEEALSO 26Thm.EQ_IMP_RULE, Drule.IMP_ANTISYM_RULE. 27\ENDDOC 28