Remove TABs from examples

futzing about with regexp test examples

Fix formal-languages/regular

Remove trailing whitespace throughout examples/

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

Changed representation of charsets to word64^4 in the ML regexp matcher.

reset permissions

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

Fixes for Poly/ML 5.7.

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.

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

Added a pretty printer and improved performance of Regexp_Match. Proof path not working at the moment.

fixed efficiency bug (in parse tree for disjoined replications like \w{1,20}

Added bitfield packing support via the \p{ ... } construct

added number literals to regexp directives

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.