History log of /seL4-l4v-10.1.1/HOL4/help/Docfiles/Q.RENAME1_TAC.doc
Revision Date Author Comments
# 6ffd8b6b 16-Jun-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Rename: qcase_tac/rename1; Q.FIND_CASE_TAC/Q.RENAME1_TAC

This use of the "case" substring was just confusing given things like
Cases_on. The "1" is there because I want to now implement a more
general version that
- deals with the issue (identified in the .doc file), where existing
names in the goal can still get in the way; and
- allows multiple subterms to be matched and renamed as a unit

Though seemingly independent, the second feature is really needed if the
first is to be done: implementing the first will require all the free
variables in a goal to be renamed away (to genvars, I expect), and then
it's impossible to ground particular matches against known free
variables.