----------------------------------------------------------------------
MK_COMB_TAC                                                   (Tactic)
----------------------------------------------------------------------
MK_COMB_TAC : tactic

SYNOPSIS
Breaks an equality between applications into two equality goals: one
for the functions, and other for the arguments.

LIBRARY
bool

KEYWORDS
tactic.

DESCRIBE
{MK_COMB_TAC} reduces a goal of the form {A ?- f x = g y} to the
goals {A ?- f = g} and {A ?- x = y}.

    A ?- f x = g y
   ===========================  MK_COMB_TAC
     A ?- f = g,   A ?- x = y




FAILURE
Fails unless the goal is equational, with both sides being applications.

SEEALSO
Thm.MK_COMB, Thm.AP_TERM, Thm.AP_THM, Tactic.AP_TERM_TAC,
Tactic.AP_THM_TAC.

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