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!

Avoid parsing incompatibilities with wordsTheory.

Added propositional logic (pedagogical example)
and updated the README. Some other files
seem to have been changed as well.

Fix up some minor syntax things that are
now out of date.

Adapting FactScript.sml to sleek new version of hwDefine. Also fixed
a looping proof ... possibly due to new improved arithmetic dp?

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).

General tidy up, including replacing the odd and ad-hoc definition of
DEL by a more conventional one (and thereby eliminating the need for
REG and REGF). README file has been updated.

Some, but not all, of the "x" value simulation problems have now gone
away.

Added SIMULATE (see README) to run Icarus Verilog and then launch GTKWave
from HOL.

Modified factorial example to dump a simulation environment as well
as just the Verilog translation of the implementation. Documented
dump_all_flag in README.

Corrected some typos and made FactScript.sml dump FACT.vl for testing.

Added MAKE_CIRCUIT that generates circuits build out of clocked dtype
registers. Details in the the updated README.

Very preliminary attempt to improve netlist synthesis by merging
combinational logic preceding a DEV into the interface to the
DEV. Goal is to cut down the number of handshakes, especially those
packaging up 'selector' logic like ``\(m,n).n`` etc.

Needs further thought and examples.

Added MAKE_NETLIST to generate netlist representations in HOL.

See README and revised FactScript.sml.

Used some old code to drag existential quantifiers to the head of a
conjunction in which I spotted the rather unacceptable:

mk_oracle_thm(Tag.read "EXISTS_OUT_CONV")([],mk_eq(t,t3))

Will need to make this respectable sometime soon. May be a performance
challenge though.

Konrad: is there something better to use off-the-shelf
(EXISTS_OUT_CONV is hol88 era code)

Revision of yesterday's version to make refinements more analogous
to conversions. I've also changed some names around (Sorry).

See README for latest stuff.

Main changes are:

1. Refine renamed to REFINE and now doesn't "depth" scan the circuit.
The scanning is done explicitly by an operator DEPTHR (which
is analogous to DEPTH_CONV).

2. Have added refinement combining operators THENR, ORELSER.

3. Lib renamed to LIB_REFINE.

4. ATMfn renamed to ATM_REFINE.

An example (see FactScript.sml) is:

REFINE
(DEPTHR(LIB_REFINE[FactIter_dev])
THENR DEPTHR(LIB_REFINE[SUBS [MultThm] Mult_dev])
THENR DEPTHR(LIB_REFINE[MultIter_dev])
THENR DEPTHR ATM_REFINE)
Fact_dev;

I hope this is converging! I should take a rest and do some more PSL
proofs now.

Added extra refinement step in FactScript.sml to convert all remaining
DEVs to ATMs.

Changed the "design flow" model to be more flexible. Hardware can now
be refined, so top-down development better supported. See README and
revised FactScript.sml example. Libraries are only used for
refinement, not in generating hardware (so library argument of
hwDefine has gone). This is experimental. Comments?

Installing KXS's hwDefine. See README.

Just realized that I don't want Holmake to compile hwdefn.sml so
am renaming it to hwdefn. Feel free to change names, etc.

Documenting Once and Ntimes reminded me of AC, and that
helped shorten the proof of correctness of FactIter.

Adding Juliano Iyoda's theory of handshaking devices and various
supporting HOL tools. See the README file. Putting the stuff here so that
Cambridge and Utah can collaborate on further developments
----------------------------------------------------------------------
composeScript.sml devScript.sml compileScript.sml CVS: compile.sml
FactScript.sml CVS:
----------------------------------------------------------------------