rhs : term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Returns the right-hand side of an equation.
DESCRIPTION
If
M
has the form
t1 = t2
then
rhs M
returns
t2
.
FAILURE
Fails if term is not an equality.
SEEALSO
lhs
,
dest_eq
HOL
Kananaskis-13