mk_eq : term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Constructs an equation.
DESCRIPTION
mk_eq(t1, t2)
returns the term
t1 = t2
.
FAILURE
Fails if the type of
t1
is not equal to that of
t2
.
SEEALSO
dest_eq
,
is_eq
HOL
Kananaskis-13