Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-01 13:39:35 -0800 (Mon, 01 Nov 1999)
Revision: 2837
Log message:

      Ran through the spell checker.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-01 17:50:29 -0800 (Mon, 01 Nov 1999)
Revision: 2838
Log message:

      Moved the complete listing of the MetaPRL font from MetaPRL System Description
      to MetaPRL User Guide and added the necessary links.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-01 18:24:19 -0800 (Mon, 01 Nov 1999)
Revision: 2839
Log message:

      Formatting fixes, several small updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-01 18:44:54 -0800 (Mon, 01 Nov 1999)
Revision: 2840
Log message:

      Small fix
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-01 18:45:45 -0800 (Mon, 01 Nov 1999)
Revision: 2841
Log message:

      Yet another small fix
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-02 18:21:17 -0800 (Tue, 02 Nov 1999)
Revision: 2842
Log message:

      Added "make realclean" target that uses CVS information and interactively removes
      all the files that have no CVS entries associated with them.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-02 21:26:11 -0800 (Tue, 02 Nov 1999)
Revision: 2843
Log message:

      Remove bin/convert on "make clean"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-05 08:47:58 -0800 (Fri, 05 Nov 1999)
Revision: 2844
Log message:

      More links
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-05 16:14:15 -0800 (Fri, 05 Nov 1999)
Revision: 2845
Log message:

      Another "small" thing that we should be more careful about when compiling rewrites.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-06 18:42:47 -0800 (Sat, 06 Nov 1999)
Revision: 2846
Log message:

      A simle implementation of data structure and functions for list permutations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-11 13:00:33 -0800 (Thu, 11 Nov 1999)
Revision: 2847
Log message:

      - Edited the autoT section a little
      - Added an empty section on dT
      - Added some problems with missing or outdated documentation to BUGS
      - Added references to tactic descriptions to User Guide.
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 1999-11-13 09:20:56 -0800 (Sat, 13 Nov 1999)
Revision: 2848
Log message:

      n*log n unifiability test
      Committing in meta-prl/refiner/term_ds/
      Added Files:
        term_unif_ds.ml
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 1999-11-14 12:56:11 -0800 (Sun, 14 Nov 1999)
Revision: 2849
Log message:

      The unify function is added into term_unif_ds. It unifies 2 terms and returnes a
      substitution.:
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-15 23:11:24 -0800 (Mon, 15 Nov 1999)
Revision: 2850
Log message:

      Added a warning about make 3.77 doing something wrong w.r.t dependencies
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-16 07:36:06 -0800 (Tue, 16 Nov 1999)
Revision: 2851
Log message:

      Fixed Makefiles for "old" theories.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-16 08:08:15 -0800 (Tue, 16 Nov 1999)
Revision: 2852
Log message:

      Fixed some problems with TPTP.
      
      create_tptp is still disabled in editor/ml/shell.ml,
      so z.ml still does not work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-16 10:25:51 -0800 (Tue, 16 Nov 1999)
Revision: 2853
Log message:

      ls takes flags string, not just unit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-16 22:34:41 -0800 (Tue, 16 Nov 1999)
Revision: 2854
Log message:

      Added debug_ascii_io
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-16 22:39:41 -0800 (Tue, 16 Nov 1999)
Revision: 2855
Log message:

      More debugging.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-21 13:56:32 -0800 (Sun, 21 Nov 1999)
Revision: 2856
Log message:

      Smaller factorial examples.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-21 14:19:12 -0800 (Sun, 21 Nov 1999)
Revision: 2857
Log message:

      BUG 2.3 now includes:
      
      Loading the same theory twice produces similar problems.
      
      As a result, `load'ing a theory and then `cd'ing into it
      (which attempts to load the theory again) does not quite work.
      As a temporary workaround, the "load" function was removed from
      toploop.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-21 16:42:26 -0800 (Sun, 21 Nov 1999)
Revision: 2858
Log message:

      Added a check that makes sure that a correct version of Ocaml and Camlp4
      is used.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-21 21:43:56 -0800 (Sun, 21 Nov 1999)
Revision: 2859
Log message:

      Made MetaPRL compatible with ocaml-2.03/camlp4-2.03
      
      At the same time it became incompatible with ocaml-2.02/camlp4-2.02...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-21 22:11:47 -0800 (Sun, 21 Nov 1999)
Revision: 2860
Log message:

      "ocamlmktop -v" bug workaround.
      
      It turned out that "ocamlmktop -v" was not only printing the version number,
      but also creating an a.out file with Ocaml toploop. After this fix, it is going
      to put that toploop into /dev/null ...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-23 14:05:41 -0800 (Tue, 23 Nov 1999)
Revision: 2861
Log message:

      Documented restriction that should we impose on internal manipulations on
      Term_ds.term objects in order to make Term_ds work safely.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-25 22:13:38 -0800 (Thu, 25 Nov 1999)
Revision: 2862
Log message:

      Updated the download documentation. Added a link to "The CVS Book".
      

Changes by: Vladimir N. Krupski (krupski at lpcs.math.msu.su)
Date: 1999-11-28 13:10:30 -0800 (Sun, 28 Nov 1999)
Revision: 2863
Log message:

      The TermSubstMm functor provides n*log n unifiability test
      and unify function time=O(#variables^2)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-11-28 18:57:22 -0800 (Sun, 28 Nov 1999)
Revision: 2864
Log message:

      Both Caml 2.04 and 2.03 may be used to compile MetaPRL