| #
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)
|
| #
07c4ff31 |
|
03-Jun-2017 |
Konrad Slind <konrad.slind@gmail.com> |
reset permissions
|
| #
3842bf8b |
|
03-Jun-2017 |
Konrad Slind <konrad.slind@gmail.com> |
speed up some proofs, adjust to IntInf, and some re-org
|
| #
42865876 |
|
22-Feb-2017 |
Konrad Slind <konrad.slind@gmail.com> |
Added some code-gen targets (java and sml). Also ruthlessly got rid of whitespace. I don't know why it is so bad, but it is gone.
|
| #
06e46592 |
|
09-Jun-2016 |
Konrad Slind <konrad.slind@gmail.com> |
Theory of regular expressions, featuring derivative-based regexp compiler which can be applied in deduction mode, or in SML mode.
|