1\DOC mk_imp 2 3\TYPE {mk_imp : term * term -> term} 4 5\SYNOPSIS 6Constructs an implication. 7 8\DESCRIBE 9If {t1} and {t2} are terms of type {bool}, then {mk_imp(t1,t2)} 10constructs the term {t1 ==> t2}. 11 12\FAILURE 13Fails if {t1} and {t2} are not both of type {bool}. 14 15\SEEALSO 16boolSyntax.dest_imp, boolSyntax.dest_imp_only, boolSyntax.is_imp, boolSyntax.is_imp_only, boolSyntax.list_mk_imp. 17\ENDDOC 18