Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-04 04:23:25 -0700 (Thu, 04 Sep 2003)
Revision: 4930
Log message:

      I have implemented parsing of the proofs and extraction of the information
      on which axioms a certain proof depends (producing an error message if
      a proof uses - directly or indirectly - a derived item that was not fully
      proven). Note that the scanning is done xon the lowest possible level (Refine
      module), so the results are high-confidence.
      

Changes	Path
+107 -33	metaprl/refiner/refiner/refine.ml
+9 -5	metaprl/refiner/refsig/refine_sig.ml
+42 -26	metaprl/support/shell/shell.ml