===============================================================================
== Examples in this directory ending ".ml" which should be run interactively ==
== (e.g. loaded with "use")                                                  ==
===============================================================================

Xor32.ml .................. Simple example showing use of AddBinop
NotXor32.ml ............... Simple example showing use of AddUnop and AddBinop
Fact32.ml ................. Factorial example using word32 
Fact32Script.ml ........... Factorial example using word32, proving relation
                            with general factorial.
exor32.ml ................. Simple example showing low-level interfaces used
                            in adding components. To be consulted when approach
                            in Xor32.ml doesn't work.

*******************************************************************************

For running interactively (see examples listed above):

 loadPath := "../" :: !loadPath;

For compilation (currently no files to compile, but need to
make word32Theory) do:
 
 Holmake 

(this uses Holmakefile).