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