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