mk_imp : term * term -> term
STRUCTURE
SYNOPSIS
Constructs an implication.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1