Simplify proofs in lift_ieeeScript.sml by removing is_normal assumption

Remove some Unicode.

Remove unicode symbols making CI fail

Add some identity properties about rounding with ties to even in src/floating-point/lift_ieeeScript.sml

Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Update floating-point theory to specify exception flags for some operations.

• The flags are: DivideByZero, InvalidOp, Overflow, Precision and Underflow.
• The arithmetic operations now return a pair (flags and result).
• Native (oracle) evaluation has been overhauled. It now only applies to some 64-bit machine_ieeeTheory operations directly.
• The L3 Importer has been updated.

Add some more floating-point theorems.

Now covers square root and fused multiply add/sub.

Add semi-colons to declarations in lift_ieee

This makes large chunks easier to cut-and-paste without running the
risk of losing a whole bunch of intermediate REPL bindings.

As per the developing Proofstyle manual, I might add.

Fix lift_ieee where overloads might resolve awkwardly

Interactive and non-interactive behaviours were distractingly
different.

Add some floating-point theorems.

Theorems from the old floatTheory have been ported to the newer floating-point theory. The results have been generalised from being single precision only, allowing them to be instantiated to 16-, 32- and 64-bit floats.