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