mk_conj : term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Constructs a conjunction.
DESCRIPTION
mk_conj(t1, t2)
returns the term
t1 /\ t2
.
FAILURE
Fails if
t1
and
t2
do not both have type
bool
.
SEEALSO
dest_conj
,
is_conj
,
list_mk_conj
,
strip_conj
HOL
Kananaskis-14