REFL : conv
STRUCTURE
Thm
SYNOPSIS
Returns theorem expressing reflexivity of equality.
DESCRIPTION
REFL
maps any term
t
to the corresponding theorem
|- t = t
.
FAILURE
Never fails.
SEEALSO
ALL_CONV
,
REFL_TAC
HOL
Kananaskis-14