EQ_IMP_RULE : thm -> thm * thm
STRUCTURE
SYNOPSIS
Derives forward and backward implication from equality of boolean terms.
DESCRIPTION
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
HOL  Trindemossen-1