REFL : term -> thm

SYNOPSIS
Returns theorem expressing reflexivity of equality.

DESCRIPTION
REFL maps any term `t` to the corresponding theorem |- t = t.

FAILURE CONDITIONS
Never fails.

EXAMPLE
  # REFL `2`;;
  val it : thm = |- 2 = 2

  # REFL `p:bool`;;
  val it : thm = |- p <=> p

COMMENTS
This is one of HOL Light's 10 primitive inference rules.

SEE ALSO
ALL_CONV, REFL_TAC.