1\DOC REFL 2 3\TYPE {REFL : conv} 4 5\SYNOPSIS 6Returns theorem expressing reflexivity of equality. 7 8\KEYWORDS 9rule, reflexive, equality. 10 11\DESCRIBE 12{REFL} maps any term {t} to the corresponding theorem {|- t = t}. 13 14\FAILURE 15Never fails. 16 17\SEEALSO 18Conv.ALL_CONV, Tactic.REFL_TAC. 19\ENDDOC 20