Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-01 17:52:07 -0700 (Tue, 01 Jun 1999)
Revision: 2682
Log message:

      Fixed a bug that prevented resulting terms from being displayed in toploop.
      
      Before:
      # <<'x>>;;
      #
      
      Now:
      # <<'x>>;;
      x : term
      #
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-01 19:16:00 -0700 (Tue, 01 Jun 1999)
Revision: 2683
Log message:

      Produce more meaningful error messges when parsing terms in toploop.
      
      Before:
      # <<x>>;;
      chars 17-18: Pcaml.Qerror("", 0, _)
      # chars 20-22: Stream.Error("illegal begin of toplevel phrase")
      #
      ...
      # <<x>>;;
      chars 57-58: Pcaml.Qerror("", 0, _)
      # chars 60-62: Stream.Error("illegal begin of toplevel phrase")
      #
      
      Now:
      # <<x>>;;
      chars 17-18: Failure("Shell_p4.mk_opname: no current package")
      # chars 20-22: Stream.Error("illegal begin of toplevel phrase")
      #
      ...
      # <<x>>;;
      chars 57-58: Failure("Package_info.mk_opname: summary not initialized")
      # chars 60-62: Stream.Error("illegal begin of toplevel phrase")
      #
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-01 22:56:08 -0700 (Tue, 01 Jun 1999)
Revision: 2684
Log message:

      1) By default, the values of non-meta string/token/var parameters are now printed in quotes
      
      2) Fixed the dispay forms for summary items. There were several problems there:
      - some display forms (id, prec_rel) were assuming wrong term structure
      - some display forms were broken by the addition of an extra resource_def argument.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-02 02:14:37 -0700 (Wed, 02 Jun 1999)
Revision: 2685
Log message:

      - added a display form for Summary!meta_function. Still, things do not
      always look right - take, for example itt_int theory, intElimination rule
      
      - copied itt_list.cmoz to itt_list.prlb to eliminate
      "rules nilFormation do not match" warning
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-02 16:01:30 -0700 (Wed, 02 Jun 1999)
Revision: 2686
Log message:

      Documentation:
      - removed references to slot[i:n], slot[t:t] and slot[v:v], mentioned that
      slot[p:s] should be used for printing parameters
      - removed var:l from the term syntax description, mentioned that :s in parameters
      is optional
      - ran spell-checker on mp-dform and mp-terms
      
      Summary:
      - added display forms for MetaLabeled
      - fixed display form for MetaFunction
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-03 00:00:22 -0700 (Thu, 03 Jun 1999)
Revision: 2687
Log message:

      Here's some documentation I wrote for the base
      tactics/conversions/etc. and for ITT.  I wrote it for myself; I hope
      other people find it useful.
      
      Let me know what you think!
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-05 02:22:02 -0700 (Sat, 05 Jun 1999)
Revision: 2688
Log message:

      Fixed minor inaccuracies in doc/it_quickref.txt.
      
      Bugfix in max_level_exp (both ds and std).
      
      Fixed precedence of "fun" constructor:
         (a -> b) -> c
      was displaying as
         a -> b -> c
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-05 03:22:13 -0700 (Sat, 05 Jun 1999)
Revision: 2689
Log message:

      Made the working directory (more easily) configurable.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-05 15:33:26 -0700 (Sat, 05 Jun 1999)
Revision: 2690
Log message:

      Added a workaround for a bug in my version of Emacs.  Shouldn't affect
      anyone else; let me know if it does, and I'll back it out.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-05 23:26:04 -0700 (Sat, 05 Jun 1999)
Revision: 2691
Log message:

      Added a new primitive rule universeCumulativity and corresponding
      tactic cumulativityT.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-06 19:56:23 -0700 (Sun, 06 Jun 1999)
Revision: 2692
Log message:

      Now that I (think I) understand "squash", I've made my new cumulativity
      rule a bit more general.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-07 20:03:21 -0700 (Mon, 07 Jun 1999)
Revision: 2693
Log message:

      Fixed some comments
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-08 16:23:41 -0700 (Tue, 08 Jun 1999)
Revision: 2694
Log message:

      Removed unused code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-08 19:19:59 -0700 (Tue, 08 Jun 1999)
Revision: 2696
Log message:

      Added a comsistent way of coming up with a new name for a variable that needs to be renamed
      (for example, to avoid capturing during substitution).
      
      Please note: the renaming algorithm is likely be changed in the future,
      no part of the system should rely on the particular algorithm.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-08 20:28:30 -0700 (Tue, 08 Jun 1999)
Revision: 2697
Log message:

      Removed duplicate code
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-08 20:44:27 -0700 (Tue, 08 Jun 1999)
Revision: 2698
Log message:

      compile_so_redex_term can not get a context term as an input (not as a part of a sequent)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-10 19:12:51 -0700 (Thu, 10 Jun 1999)
Revision: 2699
Log message:

      Backed up the previous change. We may be interested in having SO contexts
      outside sequents, but we need to implemnt them correctly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-10 19:28:03 -0700 (Thu, 10 Jun 1999)
Revision: 2700
Log message:

      Documented some rewriter bugs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-10 20:31:51 -0700 (Thu, 10 Jun 1999)
Revision: 2701
Log message:

      More rewriter bugs.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-10 22:31:14 -0700 (Thu, 10 Jun 1999)
Revision: 2702
Log message:

      Fixed level_lt and level_le.  Now the universeEquality rule no longer
      proves << member{univ[i:l]; univ[i:l]} >>, and it does prove
      << member{univ[i|j ':l]; univ[j:l]} >> (it got both of these cases
      wrong before).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-11 13:49:17 -0700 (Fri, 11 Jun 1999)
Revision: 2703
Log message:

      Fixed the "repeated meta-parameter" rewriter problem.
      However, I have not checked the level expressions code yet.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-11 17:22:28 -0700 (Fri, 11 Jun 1999)
Revision: 2704
Log message:

      More problems
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-11 18:01:46 -0700 (Fri, 11 Jun 1999)
Revision: 2705
Log message:

      Removed unused directory
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-12 19:34:07 -0700 (Sat, 12 Jun 1999)
Revision: 2706
Log message:

      Small changes
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-13 08:21:46 -0700 (Sun, 13 Jun 1999)
Revision: 2707
Log message:

      - Documented the behaviour of several functions when variable lists
      have repeated entries.
      In particular: <<x,x.'x>> is understood as <<x,y.'x>> by alpha_equality.
      
      - Made sure that this behaviour of Term_ds and Term_std is consistent
      with the documentation.
      
      - Documented a bug in alpha_equal_match
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-13 15:21:30 -0700 (Sun, 13 Jun 1999)
Revision: 2708
Log message:

      - Now rewriter should handle repeated variables in redex more or less correctly
      
      - I changed build_contractum to use String_util.vnewname for renaming variables
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-13 18:14:10 -0700 (Sun, 13 Jun 1999)
Revision: 2709
Log message:

      Changed the behavior of the dT and eqcdT tactics on goals with
      conclusions of the form
      << (quot x1, y1: 'A1 // 'E1['x; 'y]) =
         (quot x2, y2: 'A2 // 'E2['x1; 'x2]) in univ[@i:l] >>
      (to use the quotientWeakEquality rule instead of the quotientEquality
      rule).  The old behavior is recovered with altT.
      
      I would be very surprised if this broke any proofs; the original
      tactic created subgoals of the same form as the current goal, and I
      don't think there's any way to prove those subgoals.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-13 19:19:35 -0700 (Sun, 13 Jun 1999)
Revision: 2710
Log message:

      Added equalityEquality to the eqcd resource, so eqcdT and dT 0 can handle
      << ('a1 = 'b1 in 'T1) = ('a2 = 'b2 in 'T2) in univ[i:l] >>.
      
      Updated documentation.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-13 20:32:18 -0700 (Sun, 13 Jun 1999)
Revision: 2711
Log message:

      cvf_theory is not an MLZFILE and should not be mentioned in Makefile
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-13 21:03:39 -0700 (Sun, 13 Jun 1999)
Revision: 2712
Log message:

      Fixed the following behavior when using the OCaml toplevel:
      # << univ[i:l] >>;;
      Unbound constructor Refiner.Refiner.TermType.Level
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-13 21:21:47 -0700 (Sun, 13 Jun 1999)
Revision: 2713
Log message:

      - Added a "strict" flag to compile_redex. Currently rewrite.ml just always sets it
      to false, but the support for the flag is there.
      
      The free variable checking in "strict" mode would not always wor correctly when
      matching term that has repeated bound variables. I plan to fix most (hopefully all)
      bugs related to matching terms repeated bound variables in a separate commit.
      
      - Made rewrite_type_sig.mlz a generated file - it is very close to rewrite_types.ml
      and it is annoying to have to change them both every time.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-14 00:13:27 -0700 (Mon, 14 Jun 1999)
Revision: 2714
Log message:

      * Made the initialization more stable by adding a list of modules to open.
      
      * Instead of an initialization command, define a file to #use, ~/.mprc by
        default - this should probably be done by MP itself.
      
      * Some more minor changes and cosmetics.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-14 23:14:36 -0700 (Mon, 14 Jun 1999)
Revision: 2715
Log message:

      I'm going to avoid the ugly hack of translating DEFMACRO's to a
      temporary syntax by adding the macros as soon as they're parsed.
      This means that macros can be used before their definitions and that
      playing games like modifying macros for some source parts wouldn't work,
      so I'm still not sure I'll go with it, but I'm cheking this in just in
      case.
      
      If anyone thinks that such a behavior would be a bad idea, tell me.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-15 02:37:40 -0700 (Tue, 15 Jun 1999)
Revision: 2716
Log message:

      Finally, this version works with includes.
      
      Also, the ugly hack of temporary syntax trees is not needed, yet the
      processing of macros is sequential so macro redefinitions etc work
      properly.
      
      Other things that might be needed, but I'll consider them only if such
      a need arise are:
      1. Error reporting is probably heavily screwed up because of bogus loc
         fields.  I'll try to solve each problem as it pops.
      2. Making everything work also in interface files,
      3. Adding toplevel macros so a single macro application will be able to
         create several definitions (if this is implemented then INCLUDE can
         be such a macro with an ML function body).
      
      Tomorrow I'll start trying to move CPP stuff to use this instead.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-15 15:53:39 -0700 (Tue, 15 Jun 1999)
Revision: 2717
Log message:

      Added
        cd `dirname $0`
      so it is possible to run these files from any directory.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-15 23:34:45 -0700 (Tue, 15 Jun 1999)
Revision: 2718
Log message:

      Added a -I option for INCLUDE statements.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-16 12:06:59 -0700 (Wed, 16 Jun 1999)
Revision: 2719
Log message:

      Added a local macro construct.
      
      Also Added some documentation on what is provided so far.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-16 17:20:55 -0700 (Wed, 16 Jun 1999)
Revision: 2720
Log message:

      Added HashTerm and HashBTerm modules to TermHash module in order to be able to
      have hash tables with terms or bterms as keys
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 02:08:44 -0700 (Thu, 17 Jun 1999)
Revision: 2721
Log message:

      Made DEFINED symbols hold expressions so it is possible to use a "-DX=x"
      flag and a "DEFINE X = x" statement.
      
      Also, made the code-walker a seperate module.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 02:11:00 -0700 (Thu, 17 Jun 1999)
Revision: 2722
Log message:

      Renamed CPPFLAGS to PPFLAGS;
      Added CAMLP4MACRO to be used instead of CPP.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 02:18:19 -0700 (Thu, 17 Jun 1999)
Revision: 2723
Log message:

      marshal_shared.ml uses macro.ml now.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 02:22:52 -0700 (Thu, 17 Jun 1999)
Revision: 2724
Log message:

      Forgot to commit a stupid bug...
      (Sorry for all these seperate updates)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-17 15:39:51 -0700 (Thu, 17 Jun 1999)
Revision: 2725
Log message:

      Added: reduceEta is too strong
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 17:45:38 -0700 (Thu, 17 Jun 1999)
Revision: 2726
Log message:

      * Fixed some more bugs in macro.ml.
      
      * Added refine_error.mlh which is the ml equivalent of refine_error.h
        (there must be some better suffix for these, any ideas?)
      
      * Modified refine.ml so it uses macro.ml.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 18:16:11 -0700 (Thu, 17 Jun 1999)
Revision: 2727
Log message:

      I happen to come across an erroneous "#1/bin/csh"...
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 18:22:15 -0700 (Thu, 17 Jun 1999)
Revision: 2728
Log message:

      Forgot to commit this also.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-17 19:12:31 -0700 (Thu, 17 Jun 1999)
Revision: 2729
Log message:

      There is no need to use String_util.concat instead of String.concat
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-17 21:20:10 -0700 (Thu, 17 Jun 1999)
Revision: 2730
Log message:

      Used type system to enforce parameter hashing
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-17 21:25:57 -0700 (Thu, 17 Jun 1999)
Revision: 2731
Log message:

      Yet another commit before another major change.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-17 21:51:42 -0700 (Thu, 17 Jun 1999)
Revision: 2732
Log message:

      Added support for ASCII-based term IO. I tested the code a lot and it seems working,
      but it is not integrated into the system yet. And simple_name_* functions need to be
      improved if we want ASCII theory files to be at least sligtly readable.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-18 05:21:43 -0700 (Fri, 18 Jun 1999)
Revision: 2733
Log message:

      Whew...  I hope that this one is the last major rewrite for this...
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-19 17:06:36 -0700 (Sat, 19 Jun 1999)
Revision: 2734
Log message:

      Fixed alpha_equal_match
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-20 15:07:53 -0700 (Sun, 20 Jun 1999)
Revision: 2735
Log message:

      Removed some really old filter test files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-20 17:41:38 -0700 (Sun, 20 Jun 1999)
Revision: 2736
Log message:

      In "strict" mode rewriter now should correctly restrict free variables
      in sequent contexts.
      
      I postponed testing of this code until "strig" flag would be fully implemented.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-21 01:48:24 -0700 (Mon, 21 Jun 1999)
Revision: 2737
Log message:

      Now the arguments of SO variables are fully compiled and matched.
      
      As a result, the nested SO variables in a redex are now handled correctly.
      
      This also allowed to replace alpha_equal_match with a fuction alpha_equal_fun
      that (IMHO) is easier to understand and I have more confidence that I've got
      it right than I had with alpha_equal_match
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-21 07:19:13 -0700 (Mon, 21 Jun 1999)
Revision: 2738
Log message:

      More changes.
      (more to come.)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-22 08:30:58 -0700 (Tue, 22 Jun 1999)
Revision: 2739
Log message:

      Added Alexei Kopylov's implementation of the collection type.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-22 13:32:03 -0700 (Tue, 22 Jun 1999)
Revision: 2740
Log message:

      Added lots of stuff to macro.ml, so it handles many more syntax types and
      also mli files.
      
      An improvised update for refiner_verb_and_simp.txt, it should either be
      extended or deleted.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-22 13:33:49 -0700 (Tue, 22 Jun 1999)
Revision: 2741
Log message:

      Using macro.ml for this directory works.
      

Changes by: ( at unknown.email)
Date: 1999-06-22 13:33:49 -0700 (Tue, 22 Jun 1999)
Revision: 2742
Log message:

      This commit was manufactured by cvs2svn to create tag
      'meta-prl-0_5_3'.

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-06-22 21:50:29 -0700 (Tue, 22 Jun 1999)
Revision: 2743
Log message:

      This is a major release; I bumped the release number to 0.6.
      WARNING: There are major changes here, and there may be problems
         with this version that prevent you from using your old proof.
         Save your work before using this version.
      NOTE: If you decide to try this out, and you find problems,
         please(!) send me email so I can fix it.
      
      Changes:
         1. The proof structure is totally changed, so that the proof
            editor edits the raw proof extracts.  This means that you
            can view the actions of the refiner down to the primitive
            rule applications.  In the proof editor, you can use
            "down 0" (or "cd "0") to descend into the proof of a rule box.
            Primitive proofs are called "extracts", and are labeled with
            brackets (like [extract]).  To expand the extract, use the command
            "unfold ()".  You should be able to get all the way down to
            the primitive rule/rewrite applications.
      
            This also means that the format of the proof files (the .prlb
            files) has changed.  The old proof files are still valid,
            but this is a hack and will be deprecated in the next
            few months.  I haven't yet added Alexey's ASCII proof
            files, but that will come with the next release.
      
            As usual, the "undo ()" command undoes the last proof step,
            including "unfold ()".  The "nop ()" command, reset the undo
            stack.  I also added a "redo ()" command that undoes the
            last undo.
      
            There is a simple rule-box proof cache for collecting proofs
            as you edit them.  If cached proofs are available, you will
            see them in brackets (like [* # * *]) on the status line.
            I haven't yet:( added the commands to use cached proofs.
      
         2. Refiner changes.  I added two new features: the "cutT <term>"
            tactic cuts in a new assumption.  Also, you can apply
            rewrites directly on assumptions, with the "rwc" and
            "rwch" operations, that take a clause argument.  Basically,
            this means that instead of folding the goal, you can unfold
            the assumption.  I believe this is sound; let me know if
            you think otherwise!
      
         3. Resource changes.  I added resource automation, built on
            the basic resource parsing Alexey added.  Ratherthan writing
            resource code for every rule, you can annotate most rules
            to generate the resource code directly.  You can see lots of
            examples in the Itt theory.  Basically, there are three useful
            resources annotations:
               intro_resource []: adds the rule as an introduction in dT
               intro_resource [SelectOption i]: adds to selT i dT
               elim_resource []: adds as an elimination rule to dT.
                  This normally tries to thin the hyp that was eliminated.
               elim_resource [ThinOption]: don't thin the hyp
      
            Rules should be annotated with labels on their clauses,
            like [wf], [main], [assertion], etc.  This means that in
            most tactic aplcations, you no longer need to have the
            thenLT [addHiddenLabel "main"; ...] part.
      
            N.B.  This is the most likey parts of this release to
            cause problems, because I deleted most old resource code.
      
            Also, you can still write standard resource code, but there
            is no longer a d_resource--it has been broken into two parts:
            the intro_resource for application to goals, and elim_resource
            for application to hyps.
      
         4. The proof editor is multi-threaded, so you can work on multiple
            proofs simultaneously.  In the normal Emacs editor, this is
            no help for you.  But there is a new Java editor with the
            standard point-and-click interface, and it views the proof
            in HTML, with multiple windows etc.  The beautiful thing is
            that you can use display forms to add commands to edit windows.
            The sad thing is that I built it on NT, Java 1.2 is required,
            and I haven't tried the blackdown.org Java release on Linux.
            This editor is pending some bug fixes from Sun to get the
            fonts right (they call this a standard release?).
      
            In any case, here are the direct implications.  The display
            forms have an "html" mode.  The display form formatting in
            the module Rformat has been completely redone, but display
            _should_ be the same as it was before.
      
            It is likely that I will add an HTML dump, so we can send
            uneditable proofs around by email or on the web.  Check out
            the file theories/base/summary.ml to see some example HTML
            display forms.
      
            The other issue: your MetaPRL process starts a web server on
            YOUR local machine using YOUR process id on the "next" available
            TCP port, and it serves files only from the search path that you pass
            MetaPRL.  I realize that this has security implications.  This
            is necessary to get browser access to the working MetaPRL proof.
            Is this crazy?  Let me know your beliefs, religious or
            otherwise.
      
         5. There are numerous minor changes.  I redid parts of the WeakMemo,
            Term_header_constr, and TermHash.  The theories/tactic directory
            has been split into tactic/boot (which is not compiled by MetaPRL),
            and theories/tactic (which is).
      
      Jason
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 11:45:15 -0700 (Wed, 23 Jun 1999)
Revision: 2744
Log message:

      Fixed couple of typos that prevented "make opt" from working
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 15:19:48 -0700 (Wed, 23 Jun 1999)
Revision: 2745
Log message:

      Updated the ds/std and VERBOSE/SIMPLE documentation.
      
      Updated mk/make_config.sh to include in mk/config the pointers to this documentation
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 16:01:38 -0700 (Wed, 23 Jun 1999)
Revision: 2746
Log message:

      Eliminated "circular dependencies" make warnings
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 16:40:57 -0700 (Wed, 23 Jun 1999)
Revision: 2747
Log message:

      By default, run make with -s (silent) flag.
      
      This way you are able to see all the essential messages that otherwise
      would get lost among all those ocamlc & ocamlopt commands
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 16:51:04 -0700 (Wed, 23 Jun 1999)
Revision: 2748
Log message:

      Removed some old code that Eli accidentally added back
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 17:10:42 -0700 (Wed, 23 Jun 1999)
Revision: 2749
Log message:

      Eliminated a worning
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 18:00:29 -0700 (Wed, 23 Jun 1999)
Revision: 2750
Log message:

      Term_copy*_weak modules only need Term modules, not full refiners, on input
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-23 18:54:39 -0700 (Wed, 23 Jun 1999)
Revision: 2751
Log message:

      Yet more stuff - now there are also toplevel macros that can be used.
      I really hope that this is the last feature addition (in other words,
      if someone don't like these frequent updates - me neither).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-23 19:28:46 -0700 (Wed, 23 Jun 1999)
Revision: 2752
Log message:

      Made some of the "internal" stuff go away.
      
      Eli, I've made refsig gcc-preprocessed, but I hope it would be really easy to convert
      it to macros. Sorry about that.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-06-24 17:19:15 -0700 (Thu, 24 Jun 1999)
Revision: 2753
Log message:

      These are some minor changes to make things work better.  Changed
      meaning of ThinOption in elim_resource: it now means to thin the hyp
      by default, unless overridden by thinningT false.
      
      Fixed some proof operations.  Added "move_to_assum" command to take
      the current subgoal and make it an extra assumption of the entire
      proof (it may not work at the moment).
      
      ls now takes a _string_ argument.  Use ls "u";; to display only the
      unproved rules in the current module.
      
      Proved many membership variants of the standard type constructors,
      but there are a few more to go.  When you are defining theories, I
      believe you should use membership, not equality.  After all, equality
      is derivable from membership, and membership is a lot easier.
      
      Still to go: ASCII format proof files; save proofs _without_ extracts
      by default.  The expand () function does not reexpand proofs correctly.
      A few problems with proof navigation.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-06-24 17:31:48 -0700 (Thu, 24 Jun 1999)
Revision: 2754
Log message:

      Disabled web server for now.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-25 17:10:11 -0700 (Fri, 25 Jun 1999)
Revision: 2755
Log message:

      macro.ml-ified.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-25 17:36:02 -0700 (Fri, 25 Jun 1999)
Revision: 2756
Log message:

      macro.ml-ified
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-25 18:37:30 -0700 (Fri, 25 Jun 1999)
Revision: 2757
Log message:

      Mazal Tov!
      
      Done.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-25 18:38:45 -0700 (Fri, 25 Jun 1999)
Revision: 2758
Log message:

      Small changes and additions.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-25 18:55:03 -0700 (Fri, 25 Jun 1999)
Revision: 2759
Log message:

      \newcommand{\message}{Mazal Tov}
      
      The last \message was too early,
      this one is OK: \message.
      
      By this commit we're completely CPP-free.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-25 19:21:38 -0700 (Fri, 25 Jun 1999)
Revision: 2760
Log message:

      Macro cleanup: renamed some of the X1 identifiers back to X'
      and removed the macros entry from the TODO file.
      

Changes by: Eli Barzilay (eli at cs.cornell.edu)
Date: 1999-06-25 20:01:09 -0700 (Fri, 25 Jun 1999)
Revision: 2761
Log message:

      * No need for "-DMLZ".
      * Added some documentaion in macro.ml.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-25 23:26:06 -0700 (Fri, 25 Jun 1999)
Revision: 2762
Log message:

      There is no need for any tmp.mli
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-28 20:40:34 -0700 (Mon, 28 Jun 1999)
Revision: 2763
Log message:

      Removed -I $(ROOT)/lib from the INCLUDES.
      It was unnecessary since mk/rules adds -I $(ROOT)/lib to ocaml{c,opt} calls anyway.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-28 20:46:59 -0700 (Mon, 28 Jun 1999)
Revision: 2764
Log message:

      This seems to work under Linux.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-28 23:23:02 -0700 (Mon, 28 Jun 1999)
Revision: 2765
Log message:

      Small changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-06-29 13:43:13 -0700 (Tue, 29 Jun 1999)
Revision: 2766
Log message:

      Minor fixes to make Linux Makefile and shell script work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-29 18:47:15 -0700 (Tue, 29 Jun 1999)
Revision: 2767
Log message:

      Fixed some comments
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-29 23:27:09 -0700 (Tue, 29 Jun 1999)
Revision: 2768
Log message:

      Now
      #use "x.ml";;
      works again in ./mp
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-06-30 12:17:56 -0700 (Wed, 30 Jun 1999)
Revision: 2769
Log message:

      If for some reason you can not connect to port 80 on metaprl-cvs, try using port 3000 instead.
      

Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-30 21:47:18 -0700 (Wed, 30 Jun 1999)
Revision: 2770
Log message:

      I tried to make the OCaml toploop (i.e., editor/ml/mp) work.  I think
      this may be part of the solution, but somebody needs to check my work;
      I didn't really understand what I was doing here.
      
      There's still a bug: when I try to enter a term at the prompt, I get
      messages claiming that the term names are undeclared:
      
      # << unit >>;;
      # While expanding quotation "term":
      Failure: undeclared name: unit
      
      This was in a context (specifically, "itt_fset/fsub_member_intro3")
      where << unit >> should have been declared (and in fact, I don't get
      that error using mptop).