History log of /seL4-l4v-master/HOL4/examples/formal-languages/regular/regexp_mapScript.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
# 4dba4f20 03-Sep-2019 Konrad Slind <konrad.slind@gmail.com>

upgraded regexp compiler to use binary-map set to represent worklist; also proved an optimization to regexp_compareW; moved to new syntaxes for HOL stuff (Theorem, Definition, etc)