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