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 examples/formal-languages/regular for tight equality

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

Remove trailing whitespace in charsetScript.sml

* 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

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