History log of /seL4-l4v-master/HOL4/examples/dev/Fact32/NotXor32.ml
Revision Date Author Comments
# 927035f4 12-May-2008 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Updated Juliano's hardware compilation to work with wordsTheory. There are
now some nasty parser warnings with "===>", "<>" and possibly others.

The dev/booth example was/is broken (I haven't attempted to repair it).

Have updated dev/AES/word8 and Crypto/AES. Perhaps dev/AES should be removed?

The hardware compilation for Crypto/TEA and Crypto/RC6 are now broken.
Updating the Crypto examples should be straightforward. Once done I can
delete src/n_bit.


# e5af62be 06-May-2005 Mike Gordon <mjcg@cl.cam.ac.uk>

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.


# 2e3a1bf2 20-Apr-2005 Mike Gordon <mjcg@cl.cam.ac.uk>

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


# 7babd9b8 16-Apr-2005 Mike Gordon <mjcg@cl.cam.ac.uk>

Minor bugfix in vsynth.sml + improved and additional examples.