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

Optimization of proof-based regexp compiler

Restored deleted theorem used in CakeML examples

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)

Fix white-space rule violations in b48f79ea1

switched to Definition and Theorem syntax (partial). Added different signed integer encodings to Regexp_Type. (This encoding stuff is going to be moved elsewhere once some things settle.) Minor renamings.

Reconcile store_thms with diverging names in db and val binding

Delete trailing whitespace in examples

Remove TABs from examples

futzing about with regexp test examples

Fix formal-languages/regular given 93036c73b4

Export Brz_determ again

While I attempted to do this in 7d1136aaf1876807f8fe47952bd66c662f5afb47
it seems that Konrad undid it in 3842bf8b3154f38904f03cf6cbaa118bcdbc7e3f

reset permissions

speed up some proofs, adjust to IntInf, and some re-org

Export Brz_determ from regexp_compilerTheory

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.

* Moved formalization of charsets to be word64#word64#word64#word64. This
will support CakeML translation. However, the implementation of the
SML regexp compiler in Regexp_Match still uses IntInf as the representation
of charsets. It might be interesting to compare the two representations for
efficiency, but that's future work.

* Incorporated in-logic PEG parser for regexps (regexp_parserTheory).
This was renamed from reSyntax to be in line with the existing naming
scheme (pre-pending things with "regexp").

* Revised packed interval syntax \p{e_1 ... e_n} to get rid of superfluous
commas between elements, and to incorporate support for padding.

Switch regular expressions in the logic to use charset64

Revised regexp package. Now based on charsets modelled with bool[256]. Some optimizations added, and some work on packed intervals also included.

Fix regexp theories for pat_assum rename

Remove trailing whitespace in regexp_compiler thy

Theory of regular expressions, featuring derivative-based regexp compiler which can be applied in deduction mode, or in SML mode.