README
1
2===============================================================================
3== Examples in this directory ending ".ml" which should be run interactively ==
4== (e.g. loaded with "use") ==
5===============================================================================
6
7Xor32.ml .................. Simple example showing use of AddBinop
8NotXor32.ml ............... Simple example showing use of AddUnop and AddBinop
9Fact32.ml ................. Factorial example using word32
10Fact32Script.ml ........... Factorial example using word32, proving relation
11 with general factorial.
12exor32.ml ................. Simple example showing low-level interfaces used
13 in adding components. To be consulted when approach
14 in Xor32.ml doesn't work.
15
16*******************************************************************************
17
18For running interactively (see examples listed above):
19
20 loadPath := "../" :: !loadPath;
21
22For compilation (currently no files to compile, but need to
23make word32Theory) do:
24
25 Holmake
26
27(this uses Holmakefile).
28
29