Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-07 09:47:35 -0700 (Fri, 07 Sep 2001)
Revision: 3376
Log message:

      Updated the type checking judgements.
      Added a few more terms for FIR terms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-12 14:03:34 -0700 (Wed, 12 Sep 2001)
Revision: 3377
Log message:

      Improved automation on type checking rules.
      Added types to let/set Subscript terms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-12 14:43:24 -0700 (Wed, 12 Sep 2001)
Revision: 3378
Log message:

      Forgot to upload some proofs in my last commit.
      Slight change to handling of match cases.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2001-09-14 00:00:13 -0700 (Fri, 14 Sep 2001)
Revision: 3379
Log message:

      Definition of algebraic group.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2001-09-14 00:05:10 -0700 (Fri, 14 Sep 2001)
Revision: 3380
Log message:

      Definitions for set difference & Boolean set
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-14 15:45:03 -0700 (Fri, 14 Sep 2001)
Revision: 3381
Log message:

      Mc_theory now pulls together everything in
      this theory.  Fir_auto defines an automation
      tactic that can be used for evaluation.
      Also added some support for allocUnion.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-16 22:35:30 -0700 (Sun, 16 Sep 2001)
Revision: 3382
Log message:

      Added reduce_eq_atom to the reduce resource.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-16 22:37:42 -0700 (Sun, 16 Sep 2001)
Revision: 3383
Log message:

      Implemented letExt as a no-op and a made a few other minor changes.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-17 19:23:22 -0700 (Mon, 17 Sep 2001)
Revision: 3384
Log message:

      Modified some terms to work with the output
      from the mc compiler.  Still need to work on
      getting output from mc to evaluate and type check
      properly.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-19 07:01:58 -0700 (Wed, 19 Sep 2001)
Revision: 3385
Log message:

      Improved the demo theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-19 12:51:58 -0700 (Wed, 19 Sep 2001)
Revision: 3386
Log message:

      Trying to make Java editor work with JDK 1.3.1. I fixed some of the problems,
      but it still does not work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-19 13:52:46 -0700 (Wed, 19 Sep 2001)
Revision: 3387
Log message:

      More fixes.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-19 21:33:32 -0700 (Wed, 19 Sep 2001)
Revision: 3388
Log message:

      Removed fir_auto since the one automation I provided doesn't work
      effectively on actual compiler output.  Updated some comments
      and added some rewrites to evaluate output from the compiler.
      Compiler output of simple programs seems to evaluate now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-20 02:32:00 -0700 (Thu, 20 Sep 2001)
Revision: 3389
Log message:

      This makes the behaviour under JDKs 1.2.2 and 1.3.1 more similar and
      more predictable.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-20 09:53:15 -0700 (Thu, 20 Sep 2001)
Revision: 3392
Log message:

      Added GPL license info/terms to these files.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-20 10:11:28 -0700 (Thu, 20 Sep 2001)
Revision: 3393
Log message:

      Temporary workaround: load URLs in a separate thread.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-20 11:40:02 -0700 (Thu, 20 Sep 2001)
Revision: 3394
Log message:

      Reordered files, so that they are compiled strictly in the dependency order.
      (I tried compiling on MacOS X, it seems this is nececcary there).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-20 20:03:22 -0700 (Thu, 20 Sep 2001)
Revision: 3395
Log message:

      Declared terms for some more elements from the FIR.
      Updated some comments in the code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-21 07:22:55 -0700 (Fri, 21 Sep 2001)
Revision: 3396
Log message:

      - Added proper escaping of <, > and & in html Rformat output
      - Goal and Subgoal window updates are now done in separate threads
      - Updated some homepages URLs in mp-people.html
      

Changes by: ( at unknown.email)
Date: 2001-09-21 07:22:55 -0700 (Fri, 21 Sep 2001)
Revision: 3397
Log message:

      This commit was manufactured by cvs2svn to create tag
      'before_ocaml_3_02'.

Changes by: ( at unknown.email)
Date: 2001-09-21 07:22:55 -0700 (Fri, 21 Sep 2001)
Revision: 3398
Log message:

      This commit was manufactured by cvs2svn to create branch 'ocaml_3_02'.

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-21 20:23:19 -0700 (Fri, 21 Sep 2001)
Revision: 3399
Log message:

      Added myself to the list of people. :)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-09-21 21:29:45 -0700 (Fri, 21 Sep 2001)
Revision: 3400
Log message:

      Initial 3.02 version.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-09-21 21:29:50 -0700 (Fri, 21 Sep 2001)
Revision: 3401
Log message:

      Initial 3.02 version.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-09-21 21:44:03 -0700 (Fri, 21 Sep 2001)
Revision: 3402
Log message:

      Somebody changed the definition of resources.  As a result,
      the 3.02 compilation will work only if the .prl* files are removed.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-09-22 09:27:37 -0700 (Sat, 22 Sep 2001)
Revision: 3403
Log message:

      First working 3.02 version.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2001-09-23 00:25:28 -0700 (Sun, 23 Sep 2001)
Revision: 3404
Log message:

      1. Minor changes in czf_itt_group;
      2. Define subgroup and abelian group;
      3. Define cyclic subgroup and cyclic group. However, there are
         problems with the proofs in czf_itt_cyclic_subgroup.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2001-09-23 00:33:50 -0700 (Sun, 23 Sep 2001)
Revision: 3405
Log message:

      recommit .prla files
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-24 09:11:38 -0700 (Mon, 24 Sep 2001)
Revision: 3406
Log message:

      Native code compilcation works now. Unfortunatelly, the bytecode one still
      complains about the Odyl_main incompatibility...
      
      I converted the patches to "diff -u" format for consistency with the previous
      generations of patches.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-24 10:48:38 -0700 (Mon, 24 Sep 2001)
Revision: 3407
Log message:

      Bytecode compilation now works too!
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-24 11:06:35 -0700 (Mon, 24 Sep 2001)
Revision: 3408
Log message:

      Added a term for Memcpy.  No rewrites (evaluation)
      for it yet, though.
      

Changes by: ( at unknown.email)
Date: 2001-09-24 11:06:35 -0700 (Mon, 24 Sep 2001)
Revision: 3409
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-25 09:52:43 -0700 (Tue, 25 Sep 2001)
Revision: 3410
Log message:

      - Merged the Ocaml 3.02 changes
      
      - Now http server is compiled in by default, but is only started if
      the "-http true" argument is passed or MP_HTTP environment variable
      is set to "true".
      
      - A few other minor changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-25 10:14:08 -0700 (Tue, 25 Sep 2001)
Revision: 3411
Log message:

      Forgot to change.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-09-26 03:47:32 -0700 (Wed, 26 Sep 2001)
Revision: 3412
Log message:

      With Ocaml 3.02, the parser seems to consider "~" to be an ordinary letter,
      not a special symbol. This means that we now need to put spaces
      (or paranteses) around "~" when writing squiddle equality terms.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-26 17:40:57 -0700 (Wed, 26 Sep 2001)
Revision: 3413
Log message:

      Updated some comments and added some for clarification.
      Added a letSubscript rewrite.
      Added a README file to hold some general comments.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-26 22:58:02 -0700 (Wed, 26 Sep 2001)
Revision: 3414
Log message:

      Added a term for atomFloat.
      Changed even more comments to be
      more informative.  Removed most
      unknown* terms since the compiler
      no longer outputs those.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-27 23:19:57 -0700 (Thu, 27 Sep 2001)
Revision: 3415
Log message:

      Fixed some erroneous universal/existential
      qualification rules and updated other rules
      to be more consistent with how
      the FIR works in practice.
      

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2001-09-28 15:52:57 -0700 (Fri, 28 Sep 2001)
Revision: 3416
Log message:

      added jprover multiplicity limit for nuprl and cleaned up jprover/nuprl connection code
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-09-29 01:01:35 -0700 (Sat, 29 Sep 2001)
Revision: 3417
Log message:

      Entered in some final end of summer comments,
      to ease picking up the code at a later date.
      (Really, its not that bad, but this is still
      a good idea anyways.)