1\DOC
2
3\TYPE {RENAME1_TAC : term quotation -> tactic}
4
5\SYNOPSIS
6Finds an instance of a pattern in a goal, and renames to use names
7from the pattern.
8
9\KEYWORDS
10
11\DESCRIBE
12The tactic {Q.RENAME1_TAC q} is defined to be
13{
14   MATCH_RENAME_TAC q ORELSE MATCH_ASSUM_RENAME_TAC q ORELSE
15   MATCH_GOALSUB_RENAME_TAC q ORELSE MATCH_ASMSUB_RENAME_TAC q
16}
17
18
19\FAILURE
20Fails if all of the constituent tactics fail.
21
22\COMMENTS
23This tactic can be used to force a particular set of names on a goal,
24hopefully making the resulting tactic more robust in the face of
25underlying implementation changes. Note though that successful use of
26this tactic requires that the ``new'' names in the provided pattern
27really be fresh for the goal. If one is really uncertain about what
28names might be appearing in a goal, this condition may be difficult to
29ensure, particularly as the tactic only looks for one instance of the pattern at a time (but see {Q.RENAME_TAC}).
30
31This tactic is also available under the alias {bossLib.rename1}.
32
33\SEEALSO
34Q.MATCH_ASMSUB_RENAME_TAC, Q.MATCH_ASSUM_RENAME_TAC, Q.MATCH_GOALSUB_RENAME_TAC, Q.MATCH_RENAME_TAC.
35
36\ENDDOC
37