mk_imp : term * term -> term
STRUCTURE
boolSyntax
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
dest_imp, dest_imp_only, is_imp, is_imp_only, list_mk_imp
HOL  Trindemossen-1