Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-12-03 18:49:30 -0800 (Mon, 03 Dec 2001)
Revision: 3459
Log message:

      I define the Stack type as an example of
      data structure defined with records.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-12-03 19:40:48 -0800 (Mon, 03 Dec 2001)
Revision: 3460
Log message:

      I've proved ssociativity for dependent intersection.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-12-07 16:22:06 -0800 (Fri, 07 Dec 2001)
Revision: 3461
Log message:

      Somehow CVS thinks this is alive, removing.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-12-07 16:35:04 -0800 (Fri, 07 Dec 2001)
Revision: 3462
Log message:

      Fixed bug #11.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-12-07 19:17:49 -0800 (Fri, 07 Dec 2001)
Revision: 3463
Log message:

      Fixed bug #10 - now the term_match_table fall-back mechanism is more complete.
      This broke couple of proofs, I fixed them.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-12-08 19:10:53 -0800 (Sat, 08 Dec 2001)
Revision: 3464
Log message:

      Many changes:
      -  Began to redo the README file to be more useful/informative.
      -  Added a TODO file for this theory to keep track of what still
         needs to be done.
      -  Regorganized where I declared int_set and rawint_set (Mc_set).
      -  Rewrote exceptions to use RefineError where reasonable/possible.
      -  Continuing to add "conversion" functions for MC FIR types
         and MetaPRL terms.  The great majority of them are there, but
         they still need work and testing.
      -  Random updates to comments.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-12-15 07:50:32 -0800 (Sat, 15 Dec 2001)
Revision: 3469
Log message:

      Updated my line.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-12-16 12:25:09 -0800 (Sun, 16 Dec 2001)
Revision: 3471
Log message:

      A final commit before I take off for the break.
      Various minor changes and improvements.  Work
      remaining is listed in TODO.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2001-12-21 21:43:27 -0800 (Fri, 21 Dec 2001)
Revision: 3472
Log message:

      -  Removed util/Construct since it seems to be
         unnecessary for building MetaPRL with cons.
      -  Minor changes to other Conscript(s).
         Mostly formatting (changing tabs to spaces).
      -  Top level Conscript only uses the MC std. lib.
         if MC_ROOT is defined.  Before, if MC_ROOT wasn't
         defined, the -I cmd. line arguments would have
         unnecessary things like -I /lib/naml/...
      -  Minor changes to display forms in theories/mc.
      -  Minor changes to code formatting in theories/mc.
      -  Filled in missing Mc_fir_connect_* functions.
         I need to look over them at some point for
         obvious typo-bugs and perform other testing.