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

Fix proof broken by a9a7e76c12

Remove now unnecessary bindings of _ind theorems

The Definition syntax does this for free.

Cleanup of append thms for SORTED

Remove a stray trailing whitespace in examples/.../regexpScript.sml

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)

revised interval generation in Regexp_Type; added lexer generator from Scott Owens

Fix bug in proof (18934f7cf gave 2 theorems same name)

Reconcile store_thms with diverging names in db and val binding

Remove TABs from examples

Remove zip_def in regexpTheory

Closes #478

One potential issue is if computeLib/EVAL of ZIP is required to work for
lists of different lengths -- listLib's compset does not support this
(but easily could). I am guessing the regexp library does not need this
though.

Fix formal-languages/regular given 93036c73b4

Converted ML implementation of charsets to align with that used in HOL. Also replaced regexp2{c,java,sml} by a single regexp2dfa program.

reset permissions

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

Fix a regexp proof for experimental kernel

Replay of 735f8b1, which was junked by cb8925df9d

Remove DOS \n and trailing w/space in regexpScript

Replay of 5d0f97b, which was junked by cb8925df

* 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

Fix a regexp proof for experimental kernel

Unfortunately this was a case where generated names differed from kernel
to kernel.

Remove DOS \n and trailing w/space in regexpScript

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

Really fix names in regexpScript

Be more explicit with variable names to fix expk breakage

Fix regexpScript's line-endings and trailing whitespace

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