op ## : ('a -> 'b) * ('c -> 'd) -> 'a * 'c -> 'b * 'd
STRUCTURE
Lib
SYNOPSIS
Infix combinator for applying two functions to the two projections of a pair.
DESCRIPTION
An application (f ## g) (x,y) is equal to (f x, g y).
FAILURE
If f x or g y fails.
EXAMPLE
- (I ## dest_imp) (strip_forall (Term `!x y z. x /\ y ==> z /\ p`));
> val it = ([`x`, `y`, `z`], (`x /\ y`, `z /\ p`))

COMMENTS
The ## combinator can be thought of as a map operation for pairs. It is declared as a right associative infix.
SEEALSO
pair
HOL  Kananaskis-13