IMP_ANTISYM_RULE : thm -> thm -> thm
STRUCTURE
Drule
SYNOPSIS
Deduces equality of boolean terms from forward and backward implications.
DESCRIPTION
When applied to the theorems A1 |- t1 ==> t2 and A2 |- t2 ==> t1, the inference rule IMP_ANTISYM_RULE returns the theorem A1 u A2 |- t1 = t2. 
   A1 |- t1 ==> t2     A2 |- t2 ==> t1
  -------------------------------------  IMP_ANTISYM_RULE
           A1 u A2 |- t1 = t2

FAILURE
Fails unless the theorems supplied are a complementary implicative pair as indicated above.
SEEALSO
EQ_IMP_RULE, EQ_MP, EQ_TAC
HOL  Trindemossen-1