MK_PAIR : thm * thm -> thm
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Proves equality of pairs constructed from equal components.
DESCRIPTION
When applied to theorems A1 |- a = x and A2 |- b = y, the inference rule MK_PAIR returns the theorem A1 u A2 |- (a,b) = (x,y). 
    A1 |- a = x   A2 |- b = y
   ---------------------------  MK_PAIR
    A1 u A2 |- (a,b) = (x,y)

FAILURE
Fails unless both theorems are equational.
HOL  Trindemossen-1