Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-01 17:07:18 -0800 (Fri, 01 Nov 2002)
Revision: 3925
Log message:

      Documentation build system and references cleanup:
      
      - Migrated from metaprl.bib to rc.bib. rc.bib is currently maintained by several
      people (including Bob's secretary) and is likely to be of better quality (eventually?).
      
      - Moved the editor/ml/tex directory to a more appropriate doc/latex/theories/ocaml_doc
      This move is paritally done server-side, so it is *not* versioned!
      
      - We used to have two different versions of metaprl.bib and metaprl.tex, now all TeX
      inputs are in doc/latex/inputs
      
      - Merged the book compilation scripts with the Make build subsystem.
      Now the book can be built by running "make ocaml-book" from the top level.
      
      - "THEORIES=ALL" will now include ocaml_doc as well.
      
      - Ocaml book will be built with CM fonts by default. If you have Licida-Bright fonts,
      uncomment the corresponding line in doc/latex/theories/book2.tex
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-11-11 22:58:26 -0800 (Mon, 11 Nov 2002)
Revision: 3927
Log message:

      Added the following definition for the list in "itt_list2":
        1. list membership.
        2. whether the elements in one list are also in the other, i.e., whether
           the element set of one list is the "subset" of that of the other.
        3. whether two lists contain the same set of elements.
      
      "Subset" is reflexive and transitive; "sameset" is reflexive, symmetric,
      and transitive. Defined some tactics: subsetConsT, samesetRefT, samesetSymT,
      and samesetTransT.
      
      In "itt_sort", proved that the sorted list contains the same element set
      as unsorted.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-11-11 22:59:06 -0800 (Mon, 11 Nov 2002)
Revision: 3928
Log message:

      Fixed a grammar error.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-11-12 15:56:17 -0800 (Tue, 12 Nov 2002)
Revision: 3929
Log message:

      Fixed a typo.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-14 16:11:56 -0800 (Thu, 14 Nov 2002)
Revision: 3930
Log message:

      Adding the 3.06 patches. Still need to create the camlp4-3.06-plexer.patch
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-20 01:02:01 -0800 (Wed, 20 Nov 2002)
Revision: 3931
Log message:

      - backThruHyp will now work for hypotheses of the form
      all x:A. (B[x] => C)
      (where C is the conclusion which does not have free occurrences of x).
      
      Of corse, this means that sometimes too many different hyps would match and
      currently logicAutoT is likely to pick the wrong one. We should eventually
      make sure it pick the most specific match (and not just the first match it finds).
      For now, I've fixed two proofs in czf_itt_dall that broke because of that.
      
      - Simplified a few itt_list2 proofs a little (use onHypsT, hypSubstT, etc).
      
      - Added a script to start xterm with the correct font and run mpopt in it.
      
      - Added scripts for comparing the proofs status in local tree to the one
      in the latest nightly run.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-20 01:19:45 -0800 (Wed, 20 Nov 2002)
Revision: 3932
Log message:

      Simplified the proof of itt_sort/insert_mem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-20 21:08:48 -0800 (Wed, 20 Nov 2002)
Revision: 3933
Log message:

      A few mors proof updates.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-20 21:41:24 -0800 (Wed, 20 Nov 2002)
Revision: 3934
Log message:

      - Added a few citations.
      - Replaced byDefT calls with byDefsT in a few places.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-11-29 07:31:32 -0800 (Fri, 29 Nov 2002)
Revision: 3935
Log message:

      Added term comparison and (partly) multiplication support for arithT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-29 16:48:33 -0800 (Fri, 29 Nov 2002)
Revision: 3936
Log message:

      Changed the wording of the copy_proof wraning. Instead of printing
      
      > copy_proof: warning: rewrites reduce_mul_meta do not match
      
      it will now print
      
      > Copy_proof: warning: rewrite reduce_mul_meta:
      >         was recently changed, potential mismatch with an existing proof.
      
      Since people compiling MetaPRL after downloading it for the first time are
      likely to see this warning (we almost amost always have mismatches on CVS),
      the warning needs to be less confusing.
      
      I am not completely satisfied with the current wording. Can somebody
      come up with a better one?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-29 22:53:33 -0800 (Fri, 29 Nov 2002)
Revision: 3937
Log message:

      - Do not build the tutorial .ps/.pdf. First, the tutorial is just too
      outdated. Second, the tutorial has images that do not fit on the page
      and htmldoc 1.8.23 complains too much about it.
      
      - Minor updates in the System Desctription.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-30 20:28:31 -0800 (Sat, 30 Nov 2002)
Revision: 3938
Log message:

      Correct location for Ocaml patches.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-30 21:46:23 -0800 (Sat, 30 Nov 2002)
Revision: 3939
Log message:

      MetaPRL files are now at http://files.metaprl.org/, not at
      ftp://ftp.cs.cornell.edu/pub/nuprl/MetaPRL/
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-11-30 22:13:32 -0800 (Sat, 30 Nov 2002)
Revision: 3940
Log message:

      Product-free expressions work fine now.
      Polynomials (with product) have some bugs yet.
      Too slow, I have to profile it later.
      There is some problems with negative numerals, alexei, could you
      look into itt_int_arith/test6 derivation?
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-11-30 23:18:30 -0800 (Sat, 30 Nov 2002)
Revision: 3941
Log message:

      Added a big warning not to use the mp.run Ocaml toploop for proof development.