REFL_TAC : tactic
STRUCTURE
Tactic
SYNOPSIS
Solves a goal which is an equation between alpha-equivalent terms.
DESCRIPTION
When applied to a goal A ?- t = t', where t and t' are alpha-equivalent, REFL_TAC completely solves it. 
    A ?- t = t'
   =============  REFL_TAC

FAILURE
Fails unless the goal is an equation between alpha-equivalent terms.
SEEALSO
ACCEPT_TAC, MATCH_ACCEPT_TAC, REWRITE_TAC
HOL  Kananaskis-10