Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-04-05 15:28:23 -0700 (Wed, 05 Apr 2000)
Revision: 2926
Log message:

      
      
      Full first order prover for J plus (incomplete) proof reconstruction
      in LJ, LJmc and LK.
      Moreover, jprover starts from sequent
      

Changes	Path
+1 -1	metaprl/editor/ml/nuprl_jprover.ml
+1 -1	metaprl/editor/ml/nuprl_jprover.mli
+1154 -215	metaprl/refiner/reflib/jall.ml
+6 -3	metaprl/refiner/reflib/jall.mli
+75 -134	metaprl/refiner/reflib/jtunify.ml
+2 -1	metaprl/refiner/reflib/jtunify.mli
+3 -1	metaprl/theories/itt/itt_logic.ml
+3 -1	metaprl/theories/itt/itt_logic.mli