Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-06 20:35:31 -0800 (Mon, 06 Dec 2004)
Revision: 6337
Log message:
Rewrote the proof squashing code. Hopefully this will fix bug 160 and other
relatex issues.
Changes | Path |
+65 -63 | metaprl/tactics/proof/proof_boot.ml |