Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-05 13:34:43 -0700 (Sat, 05 Sep 1998)
Revision: 2454
Log message:

      Upgrade to OCaml2.0.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-05 14:02:22 -0700 (Sat, 05 Sep 1998)
Revision: 2455
Log message:

      Added version numbering.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-05 15:31:37 -0700 (Sat, 05 Sep 1998)
Revision: 2456
Log message:

      Added license headers to each of the files in preparation for
      the first major release.  The license is GNU public license; if
      any of you have problems with that, let me know right away.  When
      you add new code, you should credit yourself as the author.  When
      you modify code, you should add a "Modified by:" to the header,
      and possibly a short summary of your changes.
      
      I tried to get the Author lists as correct as I remember, but there
      are more than 550 files(!) and I may have made some mistakes. Please
      add yourself if I didn't do it right.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-07 15:02:13 -0700 (Mon, 07 Sep 1998)
Revision: 2457
Log message:

      Replaced "The Ensemble Juke Box" with "Nuprl-Light".
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-07 15:15:42 -0700 (Mon, 07 Sep 1998)
Revision: 2458
Log message:

      Removed the links to button-bar.gif image and other parts of Juke Box docs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-08 16:54:29 -0700 (Tue, 08 Sep 1998)
Revision: 2459
Log message:

      Now make should work even if CAMLP4LIB environment variable is not defined.
      Also, make clean should remove all filter/*.opt files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-08 17:19:33 -0700 (Tue, 08 Sep 1998)
Revision: 2460
Log message:

      This file is never used
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-08 17:36:55 -0700 (Tue, 08 Sep 1998)
Revision: 2461
Log message:

      More CAMLP4LIB changes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-09 11:32:46 -0700 (Wed, 09 Sep 1998)
Revision: 2462
Log message:

      Remove infix.ml on make clean
      

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-09-09 12:02:30 -0700 (Wed, 09 Sep 1998)
Revision: 2463
Log message:

      .
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-09 16:10:11 -0700 (Wed, 09 Sep 1998)
Revision: 2464
Log message:

      Fixed a small bug in the bound variable renaming.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-11 13:23:54 -0700 (Fri, 11 Sep 1998)
Revision: 2465
Log message:

      Added Nuprl5 interface to editor/ml/shell.mli
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-13 20:45:59 -0700 (Sun, 13 Sep 1998)
Revision: 2466
Log message:

      Enabled profiled build under Ocaml 2.00.
      
      Ocaml 2.00 has a bug (profiled code woul segfault), so
      you need to use my patched version of ocaml: ocaml >= 2.00-4
      I've installed ocaml-2.00-4 on Mojave.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-14 15:11:29 -0700 (Mon, 14 Sep 1998)
Revision: 2467
Log message:

      Backed my last change. I was wrong thinking there was a bug.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-14 15:47:05 -0700 (Mon, 14 Sep 1998)
Revision: 2468
Log message:

      Added the evaluator directory and moved there all the files left
      from my first (unfinished) attempt to write an evaluator.
      
      mk/config: $(ROOT)/lib should be the last include directory,
      not the first one. This allows ocamldep to produce necessary
      x.cmx: y.cmx dependencies.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-17 19:50:14 -0700 (Thu, 17 Sep 1998)
Revision: 2469
Log message:

      refiner: Added the signature files describing the minimal
      term module functionality necessary for the Term_copy module.
      
      evaluator: Added missing GPL headers
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-22 15:26:47 -0700 (Tue, 22 Sep 1998)
Revision: 2470
Log message:

      Added some documentation.  This HTML is still incomplete!  But it
      should help understand the system.  Don't bother fixing spelling, etc,
      because I will probably overwrite them when I make a final pass over
      this first version.  Feel free to add documentation of course:-)
      
      Start in doc/htmlman/default.html
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-22 16:17:25 -0700 (Tue, 22 Sep 1998)
Revision: 2471
Log message:

      license.html:
      outdated by htmlman/license.html
      
      htmlman/nl-install.html:
      Replaced the read-write CVS instructions with the read-only ones.
      Changed the download URL to ftp://ftp.cs.cornell.edu/pub/nuprl/nuprl-light/ .
      I already created that directory (with write permissions for the nuprl group)
      and moved my ocaml&camlp4 RPMs there.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-23 11:58:50 -0700 (Wed, 23 Sep 1998)
Revision: 2472
Log message:

      Removed bogus quotes from edit_cd_thm.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-23 13:34:33 -0700 (Wed, 23 Sep 1998)
Revision: 2473
Log message:

      Fixed loading in edit_list_module.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-24 11:40:03 -0700 (Thu, 24 Sep 1998)
Revision: 2474
Log message:

      Fixed edit_node to convert to ped automatically.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-28 17:05:43 -0700 (Mon, 28 Sep 1998)
Revision: 2475
Log message:

      Added Lib_term module to provide generic term functions that
      handle special terms.
      
      Nuprl5 people: you should use Lib_term.mk_term and Lib_term.dest_term
      if you want term functions that work with sequents.  Let me know if there
      is a problem; an example would help a lot.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-28 17:17:03 -0700 (Mon, 28 Sep 1998)
Revision: 2476
Log message:

      I forgot to add the FOL theory.  Sorry about that.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-28 17:33:29 -0700 (Mon, 28 Sep 1998)
Revision: 2477
Log message:

      Added some features Lori requested for the Nuprl5 editor, plus
      a syntax fix in the Fol_implies module.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-09-28 17:51:07 -0700 (Mon, 28 Sep 1998)
Revision: 2478
Log message:

      Added a local module declarations like "module TTerm = ToTerm.Term", so the
      file looks a lot better now.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-09-29 16:52:06 -0700 (Tue, 29 Sep 1998)
Revision: 2479
Log message:

      Fixed comment typo.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-09-29 17:02:51 -0700 (Tue, 29 Sep 1998)
Revision: 2480
Log message:

      Fixed an error string to print a newline.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-09-29 17:51:50 -0700 (Tue, 29 Sep 1998)
Revision: 2481
Log message:

      Made nl_version.ml depend on everything but itself and the executables, so
      repeating make does nothing new.
      At least I hope I did that - can you makefile-wizards check what I did?
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-09-29 18:34:37 -0700 (Tue, 29 Sep 1998)
Revision: 2482
Log message:

      cd is now used for all navigations, for example:
        cd "/test/test1/1/2"
      goes to the second subgoal of the first of the test1 theorem.
        cd ".."
      is the same as up 1 (which now uses cd).
        cd "..."
      is equivalent to cd "../..".
      Note: Path `normalization' is done before processing, so cd "X/.." always work.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-09-30 15:17:16 -0700 (Wed, 30 Sep 1998)
Revision: 2483
Log message:

      Fixed stupid stuff.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-09-30 15:23:03 -0700 (Wed, 30 Sep 1998)
Revision: 2484
Log message:

      Make Eli's nl_version hack work correctly (I hope)
      on both native and bytecode builds