1\DOC UNABBREV_TAC
2
3\TYPE {Q.UNABBREV_TAC : term quotation -> tactic}
4
5\SYNOPSIS
6Removes an abbreviation from a goal's assumptions by substituting it
7out.
8
9\DESCRIBE
10The argument to {UNABBREV_TAC} must be a quotation containing the name
11of a variable that is abbreviated in the current goal.  In other
12words, when calling {UNABBREV_TAC `v`}, there must be an assumption of
13the form {Abbrev(v = e)} in the goal's assumptions.  This assumption
14is removed, and all occurrences of the variable {v} in the goal are
15replaced by {e}.   If there are two abbreviation assumptions for {v}
16in the goal, the more recent is removed.
17
18\EXAMPLE
19The goal
20{
21   Abbrev(v = 2 * x + 1), v + x < 10 ?- P(v)
22}
23is transformed by {Q.UNABBREV_TAC `v`} to
24{
25   2 * x + 1 + x < 10 ?- P(2 * x + 1)
26}
27
28\FAILURE
29Fails if there is no abbreviation of the required form in the goal's
30assumptions, or if the quotation doesn't parse to a variable.
31
32\SEEALSO
33BasicProvers.Abbr, Q.ABBREV_TAC.
34
35\ENDDOC
36