Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-02-01 15:15:18 -0800 (Fri, 01 Feb 2002)
Revision: 3489
Log message:

      HTML style fixes.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-01 23:13:21 -0800 (Fri, 01 Feb 2002)
Revision: 3490
Log message:

      Added and proved complicated properties of subgroups.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-05 00:20:00 -0800 (Tue, 05 Feb 2002)
Revision: 3491
Log message:

      Proved all rules related to the properties of cyclic subgroups.
      
      TODO:
         rule lt_Id and tactic lt_IdT are better to be moved into module "itt_int_base" upon Yegor's approval.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-05 00:21:10 -0800 (Tue, 05 Feb 2002)
Revision: 3492
Log message:

      A little change in the comments.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-05 12:51:44 -0800 (Tue, 05 Feb 2002)
Revision: 3493
Log message:

      Removed rule lt_Id and tactic lt_IdT since they are provable by tactic lt_AsymT
      in module "itt_int_base".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-07 15:19:33 -0800 (Thu, 07 Feb 2002)
Revision: 3494
Log message:

      Removed tactics "op_assoc1T", "op_assoc2T" (previously as comments),
      and "id_elim2T".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-07 17:06:03 -0800 (Thu, 07 Feb 2002)
Revision: 3495
Log message:

      1. Changed the definition of cyclic groups to increase generality.
      2. Added basic properties for the changed cyclic groups.
      
      TODO:
        The property "A subgroup of a cyclic group is cyclic" is not proven and
        might need to be re-defined.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-07 17:58:08 -0800 (Thu, 07 Feb 2002)
Revision: 3496
Log message:

      Removed the property "A subgroup of a cyclic group is cyclic" since it is
      not very important and is too hard to be proven now.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-16 18:09:08 -0800 (Sat, 16 Feb 2002)
Revision: 3498
Log message:

      Changed the definition of groups completely.
      The former version is awkward for defining specific groups like
      <Z, +> and is lack of generality since only ONE general group is
      defined.
      The current version adopts a parameter which makes it capable of
      handling complicated situations.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-18 19:44:19 -0800 (Mon, 18 Feb 2002)
Revision: 3501
Log message:

      Changed the definition of subgroups to subgroup{'g; 's} where 'g, 's,
      and subgroup{'g; 's} are all labels.
      Proved the properties of subgroups with this definition.
      
      TODO:
         I would adopt another definition of subgroups where 's is a "set"
         and subgroup{'g; 's} is a "type".
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-18 20:19:26 -0800 (Mon, 18 Feb 2002)
Revision: 3502
Log message:

      Changed the definitions of cyclic subgroups and cyclic groups where
      they both have the type "set". I'm considering defining them as
      "types". So the properties are not proven in this commission. I commit
      them only to enable metaprl to compile.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-02-19 12:15:59 -0800 (Tue, 19 Feb 2002)
Revision: 3503
Log message:

      No arithT has no auto-tactics inside. It understands <,>,<=,>=,= in hyps but
      does not understand negated relations and knows nothing about conclusion.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-20 23:56:36 -0800 (Wed, 20 Feb 2002)
Revision: 3504
Log message:

      Redefined subgroups. Now subgroup{'g; 's} is a "type" where 's is the
      underlying set for the subgroup and it is no longer defined by axioms,
      but by introduction and elimination rules which make the descriptions
      and proving of subgroup-related properties more straight-forward.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-02-21 09:14:28 -0800 (Thu, 21 Feb 2002)
Revision: 3505
Log message:

      Correct proof for "test"
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-02-21 09:29:16 -0800 (Thu, 21 Feb 2002)
Revision: 3506
Log message:

      When I removed .prlb and downloaded old .prla from CVS, mp does not showed
      "test2" rule and save() failed and reported incompletness of theory.
      So I had to remove .prla also and only then "test2" appeared.
      
      Another problem: some prefix of test2 conlusion appears red in emacs(???)
      
      And finally:
      cd"/";;
      ls"itt_int_arith";; - fails with:
      ls"itt_int_arith";;
      Refine error:
           ls: unrecognized option itt_int_arith
      Uncaught exception:
      Refine_error.MakeRefineError(TermType)(AddressType).RefineError("Shell", 1).
      
      
      and this last problem holds for any theory.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-02-21 10:34:26 -0800 (Thu, 21 Feb 2002)
Revision: 3507
Log message:

      Minor clean-up.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-02-22 09:06:59 -0800 (Fri, 22 Feb 2002)
Revision: 3510
Log message:

      A small comment added in anyArithRel2geT
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-24 18:10:09 -0800 (Sun, 24 Feb 2002)
Revision: 3514
Log message:

      Added "is_dep0_dep0_dep0_dep0_term", "mk_dep0_dep0_dep0_dep0_term",
      and "dest_dep0_dep0_dep0_dep0_term" for terms with 4 subterms.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-24 18:21:06 -0800 (Sun, 24 Feb 2002)
Revision: 3515
Log message:

      Added definition for equivalence relations, which are more general
      than "equal" and are necessary in the context of groups.
      
      TODO:
         1. Might need to define functionality for equivalence relations
            and update the substitution rules.
         2. Implement equivalence class.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-24 18:24:42 -0800 (Sun, 24 Feb 2002)
Revision: 3516
Log message:

      Replaced equality relations with equivalence relations everywhere in the
      context of groups, and re-proved the rules.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-02-25 13:18:49 -0800 (Mon, 25 Feb 2002)
Revision: 3517
Log message:

      Added czf_itt_equiv to MPFILES
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2002-02-25 15:31:26 -0800 (Mon, 25 Feb 2002)
Revision: 3518
Log message:

      On the way to process relations in conclusion.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-02-26 12:21:12 -0800 (Tue, 26 Feb 2002)
Revision: 3519
Log message:

      String_util cleanup:
      
      - Removed some duplicated and unused string code.
      - Removed couple of functions from string_util that were added
      to the stdlib String module in recent versions of Ocaml
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-02-27 17:35:49 -0800 (Wed, 27 Feb 2002)
Revision: 3524
Log message:

      esquash_mem does not have to be primitive, it follows directly from esquash_elim