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