dest_eq : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Term destructor for equality.
DESCRIPTION
If
M
is the term
t1 = t2
, then
dest_eq M
returns
(t1, t2)
.
FAILURE
Fails if
M
is not an equality.
SEEALSO
mk_eq
,
is_eq
,
lhs
,
rhs
HOL
Trindemossen-1