Updating h/w synthesis stuff so that it works again.

Have added an optimized version of MAKE_CIRCUIT, called
NEW_MAKE_CIRCUIT. It should be a drop-in replacement,
although the circuits it returns are not always alpha-convertible
with those of MAKE_CIRCUIT. Please try it out ... it's much
faster (6 secs vs 45 for final call to MAKE_CIRCUIT in
dev/FactScript.sml).

Added REFINE_ALL that uses previous results of hwDefine that are now
stored in a reference hwDefineLib. See Fact.ml for an example.

Various other tweaks and improvements (e.g. refinement combinators
simplified and extended).

Proved

|- !n. FACT n < 2 ** WL ==> (FACT n = w2n(Fact32(n2w n)))

and similar results for Mult, MultIter in Fact32Script.sml.

README updated.

Various recentish changes. Fact/Fact32 examples will be developed
further, but future versions of paper.tex will probably be made in
another CVS repository hosted at Cambridge. Will keep
http://www.cl.cam.ac.uk/~mjcg/proposals/dev/ updated.

The conversion from HOL to Verilog now annotates the HDL with the HOL
source (for eyeball checking, since formal checking is
impossible). This makes the factorial example too big for the vlogger
demo software, so switched to iverilog in Fact.ml.

Lots of changes aimed at partially automating the adding of new HOL
and Verilog unary and binary operators to synthesis. Read about
AddUnop, AddBinop in README and see how they are used in Fact.ml and
Fact32/Fact32.ml

Various tweaks. Added a preliminary very version of the factorial
example that works with values of type ``:word32`` rather than with
``:num``. Needed some messy support for n-bit numerals (``0w``,
``1w``, ``2w``, ... etc).

Added support for VeriLogger (http://www.syncad.com/vlg_form.htm, I
have an old free version). Added comments to Fact.ml example showing
how to change simulator.

Improved testbench code generated by SIMULATE.

Improved waveform picture in paper.
Fact.ml generates waveform shown.

Mainly a bugfix for a nested varstruct problem spotted by Konrad
whilst compiling AES.

Also, taking the opportunity to checkin Various other tweaks
(e.g. FlipFlopT/F renamed to DtypeT/F).