History log of /seL4-l4v-master/HOL4/examples/formal-languages/context-free/precparserScript.sml
Revision Date Author Comments
# 5417af9d 31-Mar-2020 Arve Gengelbach <arve.gengelbach@it.uu.se>

remove lcsymtacs (github issue #666)

The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont


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


# 05199544 20-Sep-2015 Konrad Slind <konrad.slind@gmail.com>

playground for formal language theory developments.