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.

Remove unicode from float script.

Overhaul floatTheory.

• The proofs have been redone using more modern tactics. The script is now 1281 lines shorter.
• Uninteresting lemmas are no longer stored.
• Anti-quotations are used for some constant values. This means that floatTheory works for double precision if float_format is changed in ieeeTheory.

Fix floating-point theories in light of pat_assum rename

Some more fixes, including to a couple of examples that grep turned up
as using Infixr 450.

Remove dependence on wordTheory.

Everywhere replace prove_thm (hol88ism) with store_thm and make the
theorem RRRC1 prove 450 times faster by not just brutalising it with
ground arithmetic evaluation.

Eliminate a repeated theorem in floatScript.sml.

Add more aggressive simplification of terms involving EXP (natural number
exponentiation). This affects the behaviour both of std_ss and srw_ss().
Various proofs break, so I've fixed these.

Behzad Akbarpour's theories of floating point numbers. Some fixed point
theories to follow.