Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
REFL_TAC : tactic

SYNOPSIS
Solves a goal that 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 CONDITIONS
Fails unless the goal is an equation between alpha-equivalent terms.

SEE ALSO
ACCEPT_TAC, MATCH_ACCEPT_TAC, REWRITE_TAC.