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