#
474acc2b |
|
09-Jul-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Reorganise files under examples/miller. In particular, combine formalizeUseful, subTypeUseful and ho_proverUseful into one HurdUseful that is in its own directory. Also, put Know and Suff tactics into that library so that they don't need to be repeatedly redefined at the head of the various Script files.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
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!
|
#
e20b2c50 |
|
09-Apr-2002 |
Joe Hurd <joe@gilith.com> |
New version to track changes to raw_match.
|
#
f954b912 |
|
12-Feb-2002 |
Joe Hurd <joe@gilith.com> |
Many changes due to the removal of ETA_CONV from the standard simpset.
|
#
6821d5a8 |
|
08-Jan-2002 |
Joe Hurd <joe@gilith.com> |
This example is a verification of the Miller-Rabin probabilistic primality test incorporating version 2 of probability theory and some cute example probabilistic programs. The reason I haven't incorporated it into src/ is that it takes about 2 hours to build, and carries a lot of `baggage' from my experiments with proof tools. The most convenient way to build it is change to the examples/miller/ directory, and use the `m' bash script (it also understands `m clean' to clean the directories). If this doesn't work, or you can't do this, then there's a longer version: cd ho_prover Holmake --qof cd ../subtypes Holmake -I ../ho_prover --qof cd ../RSA Holmake --qof cd ../formalize Holmake -I ../ho_prover -I ../subtypes -I ../RSA --qof cd ../prob Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize --qof cd ../groups Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize --qof cd ../miller Holmake -I ../ho_prover -I ../subtypes -I ../RSA -I ../formalize -I ../prob -I ../groups --qof cd .. It does build RIGHT NOW, but is quite sensitive to changes in the HOL proof tools. I'll try and support it (especially if anyone uses it), but sadly it might become more trouble than it's worth.
|