#
0fc75877 |
|
30-Jul-2012 |
Ramana Kumar <ramana.kumar@gmail.com> |
change interface to add_persistent_funs (#73) and fix more calls The new interface takes a list of strings naming theorems. (The old interface took a list of (string * thm) pairs.) The new way better ensures consistency of theory development and theory load behaviour: you can no longer pass a name with a theorem that isn't actually saved under it. Theorems are looked up with DB.theorem, or failing that, DB.definition or DB.axiom. Alas, I found more examples using add_persistent_funs to add theorems in ancestor theories. Rather than modify the ancestor theories, I have opted to make the offending theories save the theorems they want to add to computeLib themselves so they have a name in the current theory to pass to add_persistent_funs. If this behavior was appropriate for patricia too (da47401) change it. Alternatively, if the ancestor theories should have exported those things for computeLib anyway, search this commit for new instances of "save_thm" to see what needs fixing.
|
#
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!
|
#
18abbe1d |
|
06-Feb-2009 |
Konrad Slind <konrad.slind@gmail.com> |
Fix to bug spotted by Anthony, whereby the induction theorem for functions defined by pattern-matching on literals was failing to be proved. Misc. simplifications to TFL code plus adding "trypluck" to Lib.
|
#
82e8f84f |
|
22-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Speed things up a little.
|
#
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.
|
#
21c8b888 |
|
18-Nov-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Minor changes and improvements.
|
#
657d6095 |
|
22-Jul-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Minor tweaks.
|
#
3dc30400 |
|
17-Jul-2005 |
Konrad Slind <konrad.slind@gmail.com> |
Forgot.
|