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