EQ_TAC : tactic

- STRUCTURE
- 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

HOL Kananaskis-14