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.

Minor changes within floating-point theory.

• The operations float_negate1985 and float_abs1985 have been removed.
• Added a predicate float_is_signalling and renamed float_some_nan to float_some_qnan.
• Fixed problem with EQ_tm and GT_tm being swapped in binary_ieeeSyntax.

Improve handling of NaNs in binary_ieeeTheory.

The choice of NaN is now a function of the operation being performed. Previously all instances of float_some_nan would be the same (for any given float type).

Make more of the floating-point library available to Moscow ML users.

Evaluation now works under Poly/ML. However, Poly/ML is needed for evaluation
using native floats (which is controlled through the "native ieee" trace).