Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 2000-02-20 05:16:33 -0800 (Sun, 20 Feb 2000)
Revision: 2897
Log message:

      tptp_prove1.ml* is a copy of tptp_prove.ml* with old unification replaced
      strightforwardly by the new correct one -- unify_mm. No optimization of
      the calls (but it should be done next).
      

Changes	Path
Added	metaprl/theories/tptp/tptp_prove1.ml
Properties	metaprl/theories/tptp/tptp_prove1.ml
Added	metaprl/theories/tptp/tptp_prove1.mli
Properties	metaprl/theories/tptp/tptp_prove1.mli