mk_imp
boolSyntax.mk_imp : term * term -> term
Constructs an implication.
If t1 and t2 are terms of type bool, then mk_imp(t1,t2)
constructs the term t1 ==> t2.
Failure
Fails if t1 and t2 are not both of type bool.
See also
boolSyntax.dest_imp,
boolSyntax.dest_imp_only,
boolSyntax.is_imp,
boolSyntax.is_imp_only,
boolSyntax.list_mk_imp