1\DOC VAR_EQ_TAC 2 3\TYPE {VAR_EQ_TAC : tactic} 4 5\SYNOPSIS 6Simplifies a goal using any assumption of 7the form {v = t} or {t = v}, where {v} is a variable 8 9\KEYWORDS 10simplification, rewriting, tactic. 11 12\DESCRIBE 13{VAR_EQ_TAC} simplifies the goal, including its assumptions, 14using one assumption of 15the form {v = t} or {t = v}, where {v} is a variable 16which is not contained in {t}. 17 18In both cases, {v} is replaced throughout by {t}, 19and the relevant assumption is deleted. 20 21\FAILURE 22{VAR_EQ_TAC} fails if there are no such assumptions 23 24\SEEALSO 25bossLib.FULL_SIMP_TAC, bossLib.ASM_SIMP_TAC, Rewrite.ASM_REWRITE_TAC 26 27\ENDDOC 28 29