MK_COMB : thm * thm -> thm
STRUCTURE
Thm
SYNOPSIS
Proves equality of combinations constructed from equal functions and operands.
DESCRIPTION
When applied to theorems A1 |- f = g and A2 |- x = y, the inference rule MK_COMB returns the theorem A1 u A2 |- f x = g y. 
    A1 |- f = g   A2 |- x = y
   ---------------------------  MK_COMB
       A1 u A2 |- f x = g y

FAILURE
Fails unless both theorems are equational and f and g are functions whose domain types are the same as the types of x and y respectively.
SEEALSO
AP_TERM, AP_THM, MK_COMB_TAC
HOL  Kananaskis-14