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