----------------------------------------------------------------------
EQ_IMP_RULE                                                      (Thm)
----------------------------------------------------------------------
EQ_IMP_RULE : thm -> thm * thm

SYNOPSIS
Derives forward and backward implication from equality of boolean terms.

KEYWORDS
rule, implication, equality.

DESCRIBE
When applied to a theorem {A |- t1 = t2}, where {t1} and {t2} both have
type {bool}, the inference rule {EQ_IMP_RULE} returns the
theorems {A |- t1 ==> t2} and {A |- t2 ==> t1}.

              A |- t1 = t2
   -----------------------------------  EQ_IMP_RULE
    A |- t1 ==> t2     A |- t2 ==> t1




FAILURE
Fails unless the conclusion of the given theorem is an equation between
boolean terms.

SEEALSO
Thm.EQ_MP, Tactic.EQ_TAC, Drule.IMP_ANTISYM_RULE.

----------------------------------------------------------------------