Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-08-03 06:42:06 -0700 (Wed, 03 Aug 2005)
Revision: 7672
Log message:

      The latest change to lm_lexer.ml (that fixed a regexp bug that was reported
      for OMake) have changed the magic number. Updading the magic number.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-08-04 09:24:11 -0700 (Thu, 04 Aug 2005)
Revision: 7673
Log message:

      Text from last week.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-08-05 10:50:59 -0700 (Fri, 05 Aug 2005)
Revision: 7674
Log message:

      Minimal changes for compatibility with omake 0.9.7.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-08-05 10:52:51 -0700 (Fri, 05 Aug 2005)
Revision: 7675
Log message:

      Revised chapters on modules and compilation units.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-08-05 11:04:12 -0700 (Fri, 05 Aug 2005)
Revision: 7676
Log message:

      Print flag should be public for compatibility.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-08-05 11:05:30 -0700 (Fri, 05 Aug 2005)
Revision: 7677
Log message:

      Forgot to add these files.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-08-05 12:12:34 -0700 (Fri, 05 Aug 2005)
Revision: 7678
Log message:

      More compatibility changes.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-08-16 17:06:35 -0700 (Tue, 16 Aug 2005)
Revision: 7679
Log message:

      NetaPRL is compatible with OCaml 3.08.4
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-08-26 15:21:55 -0700 (Fri, 26 Aug 2005)
Revision: 7682
Log message:

      Bumping the MP_VERSION from 0.9.6.1+ to 0.9.6.2+
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-28 21:53:50 -0700 (Sun, 28 Aug 2005)
Revision: 7686
Log message:

      Added a module for language defintion, but it probably won't work -- the
      induction rule with this definition might not be provable
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-29 01:36:00 -0700 (Mon, 29 Aug 2005)
Revision: 7687
Log message:

      Another way defining language
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-29 17:49:42 -0700 (Mon, 29 Aug 2005)
Revision: 7688
Log message:

      Proved rules for Lang{'ops}, including the induction rule
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-08-31 01:34:53 -0700 (Wed, 31 Aug 2005)
Revision: 7689
Log message:

      Tha name of the file needs to be public for some reason.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-31 02:15:09 -0700 (Wed, 31 Aug 2005)
Revision: 7690
Log message:

      Added a theory for computational support for operators.
      
      TODO: There is a bug in the reduction of "shape{op}" - How to make an int
            into a term? To be fixed
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-31 09:52:09 -0700 (Wed, 31 Aug 2005)
Revision: 7691
Log message:

      Changed base_reflection_hoas to base_operator
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-31 10:05:59 -0700 (Wed, 31 Aug 2005)
Revision: 7692
Log message:

      remove base_reflection_hoas
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-08-31 14:13:54 -0700 (Wed, 31 Aug 2005)
Revision: 7693
Log message:

      Added support for computational operations on operators