Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Trivial mods.

Changed inlineCompile to accept Let-exps.
Also updating Mike's change to COMB_SYNTH_CONV to deal
with more cases involving tuples.

Update booth multiplier
to use the new Verilog back-end

Changed the proof in RecCompileConvert to a (hopefully) more general one able that accepts the interface of APPLY_NEXTd (Booth multiplier example).

Have changed the way inputs and outputs are split by MAKE_NETLIST and
MAKE_CIRCUIT. This is partly to improve the circuits (fewer variables)
and partly to make the representation in HOL closer to Verilog. A
benificial side-effect is that the code is simpler (and probably more
efficient - ABS_IN_OUT_SPLIT_CONV has gone, for example). See README
for updated descriptions. Note that synthesis to Verilog (vsynth.sml)
is broken -- but I'm revising that so that separate modules are
generated for the design and the stimulus (i.e. environment). Will fix
soon(ish).

Tidying up.

Some tweaks, and rollback to (hopefully) working version of MAKE_CIRCUIT.

Fix to badly generated boothDevTheory.sig file.

Booth multiplier example. Original code by Anthony Fox (part of his
ARM6 verification) was modified by Juliano Iyoda for hardware
synthesis.

The example is not yet complete but is being used by MJCG to
stress-test the hardware compiler.

There is a weird bug causing compilation (Holmake -I word32 -I .. -I
../dff) with the following error.

Exporting theory "boothDev" ... done.
Theory "boothDev" took 62.022s to build
Analysing boothDevTheory.sml
Analysing boothDevTheory.sig
File "boothDevTheory", line 493, characters 78-79:
! count1).
! ^
! Lexical error: ill-formed token

Holdep failed.


We are not sure if this is a problem in the example, or an obscure HOL
bug.