Clean up optionScript in a variety of ways

One in particular: there is now no use of adjoin_to_sml.

Fix Unicode problem in 827420bf5f

Add a couple of (automatic) rewrites about OPTION_MAP and OPTREL

Add a couple of (automatic) rewrites about OPTION_MAP and OPTREL

Remove older of Theorem syntaxes (the one with the quotes)

It's confusing to allow two, and it seems pretty clear that the
Proof-QED proof is nicer.

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

Add some theorems to optionTheory from CakeML

Move some theorems into HOL from CakeML

Touched theories include alist, list, option, pred_set.

Make core option-monad constants automatically EVAL

With few selftests

Fix typo and other errors

introduced in 81b42b0ba8065281ae101db3cc8e0b75f373bde6

Add OPTION_BIND_def to computeLib functions, add a regression test in selftest.ml. Closes #557

Remove TABs from src

Will also make selftest to check that they aren't introduced

Generate "standard" datatype simpl rewrites as tyinfos are loaded

This saves us from having to write them out to disk, which can make
for unnecessarily large theory.dat files.

Use TypeBase.export to avoid adjoin_to_theory calls

Still need to use the same facility in the implementation of Datatype.

Move smpp to Portable - get everything up to arithmeticScript working

Rename TypeBase entrypoints for caseeqsplit and friends

Now use case_eq everywhere.

Work on github issue #345

Automatically prove "case-eqsplit" theorems and store in TypeBase

For :num, this theorem looks like

(num_CASE n zc sc = v) <=>
(n = 0) ∧ (zc = v) ∨ ∃x. (n = SUC x) ∧ (sc x = v)

Such theorems can be powerful rewrites when (large) case-expressions
are asserted to be equal to some value or other.

These theorems have to be installed somewhat by hand for early types,
but from list onwards, the Datatype package handles this. This work
leverages earlier work done implementing prove_case_eq_thm (8f16922426).

Take the opportunity to rework TypeBasePure's code to use
FunctionalRecordUpdate.

This is progress with github issue #345.

Move pair, one, sum and option into one combined coretypes directory