MK_COMB : thm * thm -> thm
A1 |- f = g A2 |- x = y --------------------------- MK_COMB A1 u A2 |- f x = g y
# let th1 = ABS `n:num` (ARITH_RULE `SUC n = n + 1`) and th2 = NUM_REDUCE_CONV `2 + 2`;; val th1 : thm = |- (\n. SUC n) = (\n. n + 1) val th2 : thm = |- 2 + 2 = 4 # let th3 = MK_COMB(th1,th2);; val th3 : thm = |- (\n. SUC n) (2 + 2) = (\n. n + 1) 4 # let th1 = NOT_DEF and th2 = TAUT `p /\ p <=> p`;; val th1 : thm = |- (~) = (\p. p ==> F) val th2 : thm = |- p /\ p <=> p # MK_COMB(th1,th2);; val it : thm = |- ~(p /\ p) <=> (\p. p ==> F) p