Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-01 18:04:50 -0700 (Fri, 01 Oct 2004)
Revision: 6211
Log message:

      Proved couple more induction principles (with Xin's help).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-04 01:59:01 -0700 (Mon, 04 Oct 2004)
Revision: 6214
Log message:

      Added a quotient elimination for squiddle equality (for Yegor).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-07 19:52:24 -0700 (Thu, 07 Oct 2004)
Revision: 6220
Log message:

      mp.opt expects MP_ROOT to be set.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-07 22:25:26 -0700 (Thu, 07 Oct 2004)
Revision: 6221
Log message:

      Fixed bug 327 - added sequents supprot to TermMan.free_meta_variables.
      (Note - this function is only ever used by JProver, it's an informal hack
      to work around JProver deficiencies).
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-08 19:04:25 -0700 (Fri, 08 Oct 2004)
Revision: 6222
Log message:

      Working on rewrite-based normalization of terms (polynomials) over rationals.
      I actually have some problems that I'll post to the newsgroup.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-08 19:17:59 -0700 (Fri, 08 Oct 2004)
Revision: 6223
Log message:

      Forgot .prla
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-09 16:28:53 -0700 (Sat, 09 Oct 2004)
Revision: 6224
Log message:

      repeatC used to always do at least two identity steps in the end.
      Changing it so that it only does at most one.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-09 20:57:16 -0700 (Sat, 09 Oct 2004)
Revision: 6225
Log message:

      Replaced quotient-based definition with subset-based.
      It does not normalizes rational number representation after each operation yet.
      I commit it because I think I found a bug in the rewriter.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 18:49:09 -0700 (Sun, 10 Oct 2004)
Revision: 6226
Log message:

      Sligthly nicer display from for spread.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 18:52:35 -0700 (Sun, 10 Oct 2004)
Revision: 6227
Log message:

      Remove macropp on "omake clean"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 19:59:02 -0700 (Sun, 10 Oct 2004)
Revision: 6228
Log message:

      Only compare the binary name from the command line with "mp.opt"/"mp.top"
      when "!omake" is used, not as startup. This is necessary to avoid an annoying
      warning when using the mp.run binary.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 20:46:26 -0700 (Sun, 10 Oct 2004)
Revision: 6229
Log message:

      (Bug 330) When coming up with variable names for bound variables, it used
      to be the case that we did not take precautions against clashes within the bvars
      list of a single bterm. This commit fixes this problem.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-10 21:21:54 -0700 (Sun, 10 Oct 2004)
Revision: 6230
Log message:

      A few updates to how contexts are handled in display forms:
      - Allow free context parameters on the RHS on informal rewrites.
      - When parsing display forms, deduce the default context parameters
      for the whole display form at once, instead of seperately for each part of it.
      

Changes by: ( at unknown.email)
Date: 2004-10-10 22:34:11 -0700 (Sun, 10 Oct 2004)
Revision: 6232
Log message:

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 03:10:37 -0700 (Mon, 11 Oct 2004)
Revision: 6233
Log message:

      I've merged the new_parser branch with the trunk. I am putting the result
      of the merge onto a new branch - "new_parser2" as there seems to be a few
      issues with it.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 03:13:25 -0700 (Mon, 11 Oct 2004)
Revision: 6234
Log message:

      In my previous commit I've accidentally committed the new files onto
      the trunk, removing them from the trunk for now.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 03:27:47 -0700 (Mon, 11 Oct 2004)
Revision: 6235
Log message:

      Re-adding files properly onto the new_parser2 branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-11 20:43:21 -0700 (Mon, 11 Oct 2004)
Revision: 6237
Log message:

      - (Bug 303) Made sure that in shell_p4 (AKA editor/ml/mp AKA mp.run)
      synchronize and unsynchronize are properly matched.
      
      - Use shell_p4 to open the basic modules (this way the basic commands
      such as cd, ls, etc are available w/o having to #use "x.ml").
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-10-12 01:45:01 -0700 (Tue, 12 Oct 2004)
Revision: 6238
Log message:

      Added all basic stuff for itt_reflection, including arities of bterms
      and elimination on bterms.
      
      In Base_reflection, a simple_bterm does not have to be a bterm.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-12 13:14:30 -0700 (Tue, 12 Oct 2004)
Revision: 6239
Log message:

      Made sure theories.pdf compiles.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-15 16:22:40 -0700 (Fri, 15 Oct 2004)
Revision: 6241
Log message:

      The tests that require ITT should not be compiled unless ITT is listed in
      the THEORIES variable.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-15 16:28:44 -0700 (Fri, 15 Oct 2004)
Revision: 6242
Log message:

      Fixing a typo in my previous commit.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-15 17:45:47 -0700 (Fri, 15 Oct 2004)
Revision: 6243
Log message:

      Made sure CIC compiles.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-17 18:02:23 -0700 (Sun, 17 Oct 2004)
Revision: 6244
Log message:

      1. Addressing the bug 322 (first part about nat)
      2. Rationals are normalized pairs of integers now (gcd=1)
      3. Rational polynomial normalization
      ToDo: Grounding intermediate assertion of SupInf.
      Doing this efficently is somewhat challenging.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-17 20:07:48 -0700 (Sun, 17 Oct 2004)
Revision: 6245
Log message:

      itt_int_arith - fixing a bug discovered while doing normalization for rationals
      itt_rat2 - improvement of the treatment for this bug
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-18 05:29:18 -0700 (Mon, 18 Oct 2004)
Revision: 6246
Log message:

      Forgot to commit yesterday
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-21 12:31:10 -0700 (Thu, 21 Oct 2004)
Revision: 6247
Log message:

      Forgot to remove temporary debug code. Sorry.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-22 16:07:58 -0700 (Fri, 22 Oct 2004)
Revision: 6248
Log message:

      A bit of standartization of debug variables:
      - the "debug_foo" variable should have debug_name set to "foo", not "debug_foo"
        (less typing on the command line this way)
      - debug_description should be the same for all the instances of the same variable
        and it should be sufficiently descriptive to be meaningful w/o knowing which
        file it came from (see http://metaprl.org/developer-guide/debugging.html)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-10-22 16:14:36 -0700 (Fri, 22 Oct 2004)
Revision: 6249
Log message:

      (Bug 322) Itt_nat.nat2ge should not change the type from nat to int.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-22 20:29:30 -0700 (Fri, 22 Oct 2004)
Revision: 6253
Log message:

      With this fix arithT does not fail on /itt_nat/natFullInduction/1/1/1 even without
      last Aleksey's commit. See bug 322 for more comments.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-29 10:15:52 -0700 (Fri, 29 Oct 2004)
Revision: 6254
Log message:

      1.Added "nat{'n} in hyps" to ge_elim resource for Arith.
      2.As far as I understand indEquality was missing positivity hypothesis in the induction step subgoal.
      Luckily the proof didn't break when I've added that missing hyp.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-10-30 14:05:55 -0700 (Sat, 30 Oct 2004)
Revision: 6255
Log message:

      Fixes for proofs broken by a change in Itt_nat.indEquality made yesterday.