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

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.

added C test file gneration for existing test regexps.

Added C code generation capability. Invoked via regexp2c <name> "<regexp>".

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