#
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.
|