Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-08-17 00:16:06 -0700 (Thu, 17 Aug 2000)
Revision: 3049
Log message:
- Do not go to proof cache for non-interactive proof steps (Jason, do youu agree
with this change to proof_boot)?
- By default, do not print debugging messages from jall
- When printing addresses, start numbering hyps from 1, not 0.
- Added "rev" list revercing operation. We need to implement rewrites properly
and/or add rewriting using equality in order to be able to prove the properties
of list functions in some reasonable way.
Changes | Path |
+86 -46 | metaprl/filter/boot/proof_boot.ml |
+70 -60 | metaprl/refiner/reflib/jall.ml |
+2 -2 | metaprl/refiner/term_ds/term_addr_ds.ml |
+33 -1 | metaprl/theories/itt/itt_list2.ml |