Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-01 15:11:28 -0700 (Thu, 01 Oct 1998)
Revision: 2485
Log message:

      Use dest_simple_bterm bt instead of (dest_bterm bt).bterm in
      compare_bterm_lists
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-05 08:56:29 -0700 (Mon, 05 Oct 1998)
Revision: 2486
Log message:

      Modified Shell.edit_create_thm _not_ to take an initial sequent.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-10-05 10:42:34 -0700 (Mon, 05 Oct 1998)
Revision: 2487
Log message:

      Added library_eval (moved from ../../library because of
      dependency on nl functions).
      Modified library_eval and added library_test to support
      interaction with Nuprl 5 interface.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-10-05 10:43:15 -0700 (Mon, 05 Oct 1998)
Revision: 2488
Log message:

      Removed library_eval since it was moved to editor/ml/.
      Implemented support for link to nuprl 5 library and
      refinement editor.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-05 13:18:25 -0700 (Mon, 05 Oct 1998)
Revision: 2489
Log message:

      Updated CVS instructions in order to reflect the name change
      Nuprl-Light -> MetaPRL.
      I already renamed the directories on the CVS and FTP servers
      and created the nuprl-light links for backward compatibility.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-06 07:08:25 -0700 (Tue, 06 Oct 1998)
Revision: 2490
Log message:

      Added evaluation functions to ShellP4.
      Lori: the "open" functions do not work in edit_cd_thm.  I believe
      that the "open" expresssions are evaluated in a separate toploop,
      so there is no way to open the module in the real toploop
      except by typing it in...
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-06 12:54:12 -0700 (Tue, 06 Oct 1998)
Revision: 2491
Log message:

      Added the display form functions for Nuprl5.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-10-07 03:36:23 -0700 (Wed, 07 Oct 1998)
Revision: 2492
Log message:

      A [not-so] small mode to make nuprl-light navigation easy.
      Should work for most Emacs configurations.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-12 15:40:01 -0700 (Mon, 12 Oct 1998)
Revision: 2493
Log message:

      Added "reflection" theory, for reflecting sentences in the meta-logic
      into the Nuprl type theory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-12 18:14:08 -0700 (Mon, 12 Oct 1998)
Revision: 2494
Log message:

      I changed all the obvious places of Nuprl-Light, NL, nl, or any
      other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
      but I'll fix them soon.  As usual, let me know if anything breaks.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-12 18:25:01 -0700 (Mon, 12 Oct 1998)
Revision: 2495
Log message:

      mk/config:
       - OCAMLDEPFLAGS was overwritten here and all these "-prl" were not
         passed to ocamldep, so we were loosing lots of dependencies - fixed
       - When Makefile.dep is missing, it will be generated automatically.
      
      README, doc/htmlman/mp-install.html
       - Now there is no need to call make depend before make
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-12 18:42:52 -0700 (Mon, 12 Oct 1998)
Revision: 2496
Log message:

      "make clean" should remove *.o files
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-12 18:52:18 -0700 (Mon, 12 Oct 1998)
Revision: 2497
Log message:

      Renaming it in Makefiles:
      NLLIB -> MPLIB, NLFILES -> MPFILES, NL2FILES -> MP2FILES, etc.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-12 19:19:13 -0700 (Mon, 12 Oct 1998)
Revision: 2498
Log message:

      - Nl_debug -> Mp_debug
      - remove generated file theories/tptp/tptp_lex.ml on "make clean"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-12 19:25:02 -0700 (Mon, 12 Oct 1998)
Revision: 2499
Log message:

      Nl_resource -> Mp_resource
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-12 19:30:23 -0700 (Mon, 12 Oct 1998)
Revision: 2500
Log message:

      Environment variables now begin with MP_ instead of NL_.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-12 19:56:36 -0700 (Mon, 12 Oct 1998)
Revision: 2501
Log message:

      NLBIN -> MPBIN, NL_TPTP -> MP_TPTP
      Do not forget to change your environment variables
      and your ~/.login, ~/.*rc files
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-13 02:01:06 -0700 (Tue, 13 Oct 1998)
Revision: 2502
Log message:

      More NL -> MP changes
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-13 05:17:44 -0700 (Tue, 13 Oct 1998)
Revision: 2503
Log message:

      Removed libpthread.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-13 05:21:27 -0700 (Tue, 13 Oct 1998)
Revision: 2504
Log message:

      Renamed nl12 font to mp12.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-13 05:33:24 -0700 (Tue, 13 Oct 1998)
Revision: 2505
Log message:

      More NL->MP changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-13 10:30:37 -0700 (Tue, 13 Oct 1998)
Revision: 2506
Log message:

      Romoved all references to libpthread (target: pthread)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-13 10:35:15 -0700 (Tue, 13 Oct 1998)
Revision: 2507
Log message:

      nl12 -> mp12
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-13 12:01:22 -0700 (Tue, 13 Oct 1998)
Revision: 2508
Log message:

      Remove Makefile.dep on "make clean"
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-10-13 12:49:12 -0700 (Tue, 13 Oct 1998)
Revision: 2509
Log message:

      Modified library_eval and library_test to reflect
      renaming to MetaPRL.
      NuprlLight->MetaPRL, nl->mp, nuprl-light->meta-prl
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-10-13 13:56:47 -0700 (Tue, 13 Oct 1998)
Revision: 2510
Log message:

      Changed NL --> ML.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-10-13 14:09:47 -0700 (Tue, 13 Oct 1998)
Revision: 2511
Log message:

      Fixed mp undefined error so compiles.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-13 14:31:37 -0700 (Tue, 13 Oct 1998)
Revision: 2512
Log message:

      For removing files, always use $(RM)
      RM is currently defined in mk/config to be "rm -f"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-13 14:37:53 -0700 (Tue, 13 Oct 1998)
Revision: 2513
Log message:

      Start "make clean" by cleaning lib and bin
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-10-13 14:54:52 -0700 (Tue, 13 Oct 1998)
Revision: 2514
Log message:

      Use "make -C $$i" instead of "cd $$i; make" to avoid problems in case directory
      does not exist.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-15 10:34:04 -0700 (Thu, 15 Oct 1998)
Revision: 2515
Log message:

      Intermediate commit on tutorial.  Its still not complete.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-15 14:38:11 -0700 (Thu, 15 Oct 1998)
Revision: 2516
Log message:

      Small change to delay tactic computations.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1998-10-20 13:32:41 -0700 (Tue, 20 Oct 1998)
Revision: 2517
Log message:

      Small fixes.  You are welcome to try it - I tested it with a bare Emacs and it
      works fine.  Just load it and M-x meta-prl.