REFL_TAC : tactic

- STRUCTURE
- 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

HOL Kananaskis-14