----------------------------------------------------------------------
AP_THM_TAC                                                    (Tactic)
----------------------------------------------------------------------
AP_THM_TAC : tactic

SYNOPSIS
Strips identical operands from functions on both sides of an equation.

LIBRARY
bool

KEYWORDS
tactic.

DESCRIBE
When applied to a goal of the form {A ?- f x = g x}, the tactic {AP_THM_TAC}
strips away the operands of the function application:

    A ?- f x = g x
   ================  AP_THM_TAC
      A ?- f = g




FAILURE
Fails unless the goal has the above form, namely an equation both sides of
which consist of function applications to the same arguments.

SEEALSO
Thm.AP_TERM, Tactic.AP_TERM_TAC, Thm.AP_THM, Tactic.MK_COMB_TAC,
Tactic.ABS_TAC, Drule.EXT.

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