Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-01-15 16:03:58 -0800 (Tue, 15 Jan 2002)
Revision: 3476
Log message:

      A few HTML style changes to make it more conformant to HTML spec.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-01-18 08:35:35 -0800 (Fri, 18 Jan 2002)
Revision: 3477
Log message:

      1. Re-exported fir_eval.prla.
      2. Mc_set : minor display form change.
      3. Randomly reformatted some Conscripts it seems.
         (I removed tab characters from the files.)
      
      The next steps will be to:
      1. Consider renaming all files in theories/mc
         to start with mp_ or some other "unique" prefix
         so that the naming is consistant
         and avoids conflicts with files in MC.
      2. Begin testing the mc_fir_connect code.  This
         will probably take some time to get completely
         correct.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-01-22 15:38:59 -0800 (Tue, 22 Jan 2002)
Revision: 3478
Log message:

      1) The main Conscript has been modified.  Added lines for CPP so that MC
         compiles properly from MetaPRL.
      2) Renamed some files in theories/mc/ so as to not confliced with
         files in MC.  I've chosen the (arguably atrocious) prefix
         of mp_mc_.
      
      Assuming string_util.ml and rformat.ml, in the MC source tree,
      are renamed to something else and the changes propagated as
      necessary, this commit should re-enable MetaPRL and MC to build together
      (using cons).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-01-23 21:49:15 -0800 (Wed, 23 Jan 2002)
Revision: 3479
Log message:

      Two changes essentially:
      1) Moved more files in theories/mc to have
         the mp_mc_ prefix.
      2) Added theories/mc/tests/  The files there are
         pretty empty right now, but the idea is to put
         code there for a simple test program to test
         the mp_mc_connect modules.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-01-24 17:27:28 -0800 (Thu, 24 Jan 2002)
Revision: 3480
Log message:

      1) Added some test cases to demonstrate what
         the test program will do.
      2) Added mp_mc_compile.  This module will (hopefully)
         be used as the main interface to MC.  Right now,
         it only defines one function, compile, which
         is the identity on an Fir.prog.
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-01-28 01:59:33 -0800 (Mon, 28 Jan 2002)
Revision: 3482
Log message:

      Adding test cases for the MC connect code.
      Slight change to INCPATH in Conscript to ensure
      that the MC std. lib. is included first
      (if we're compiling with MC).
      

Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-01-28 17:51:50 -0800 (Mon, 28 Jan 2002)
Revision: 3483
Log message:

      Adding more test cases.  Some of the cases
      have already hilighted some bugs (which
      I need to track down and fix).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-01-29 16:36:09 -0800 (Tue, 29 Jan 2002)
Revision: 3484
Log message:

      Now a workable version for groups and cyclic subgroups. Rules proved, examples  added.
      Problems left:
         The proofs for rules "power_property1", "power_property2", and "power_simplify" are not yet finished because of some itt problems.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-01-29 16:42:11 -0800 (Tue, 29 Jan 2002)
Revision: 3485
Log message:

      Removing some comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-01-29 18:01:20 -0800 (Tue, 29 Jan 2002)
Revision: 3486
Log message:

      1. Adopted a new representation for cyclic groups to avoid confusion.
      2. Added the definition of cyclic groups.
      3. Added the properties of cyclic groups.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-01-30 00:41:01 -0800 (Wed, 30 Jan 2002)
Revision: 3487
Log message:

      Removed some comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-01-30 14:36:50 -0800 (Wed, 30 Jan 2002)
Revision: 3488
Log message:

      1. Small modifications in the proofs for "power_property2".
      2. Changed the definition of cyclic subgroups to increase generality.
      3. Added (more) properties for the changed cyclic subgroups.