EQ_TAC : tactic
STRUCTURE
Tactic
SYNOPSIS
Reduces goal of equality of boolean terms to forward and backward implication.
DESCRIPTION
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
HOL
Kananaskis-14