[nogin] HTML style fixes._ Mon Sep 19 03:16:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-30-079523000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-30-079523000-PDT.html [xiny] Added and proved complicated properties of subgroups._ Mon Sep 19 03:16:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-31-110004000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-31-110004000-PDT.html [xiny] Proved all rules related to the properties of cyclic subgroups._ Mon Sep 19 03:16:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-31-929024000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-31-929024000-PDT.html [xiny] A little change in the comments._ Mon Sep 19 03:16:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-33-680608000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-33-680608000-PDT.html [xiny] Removed rule lt_Id and tactic lt_IdT since they are provable by tactic lt_AsymT_ Mon Sep 19 03:16:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-34-035265000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-34-035265000-PDT.html [xiny] Removed tactics _op_assoc1T_, _op_assoc2T_ _previously as comments_,_ Mon Sep 19 03:16:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-35-230178000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-35-230178000-PDT.html [xiny] 1. Changed the definition of cyclic groups to increase generality._ Mon Sep 19 03:16:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-36-374262000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-36-374262000-PDT.html [xiny] Removed the property _A subgroup of a cyclic group is cyclic_ since it is_ Mon Sep 19 03:16:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-37-762888000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-37-762888000-PDT.html [xiny] Changed the definition of groups completely._ Mon Sep 19 03:16:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-39-048773000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-39-048773000-PDT.html [xiny] Changed the definition of subgroups to subgroup__g_ _s_ where _g, _s,_ Mon Sep 19 03:16:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-48-000462000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-48-000462000-PDT.html [xiny] Changed the definitions of cyclic subgroups and cyclic groups where_ Mon Sep 19 03:16:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-49-799287000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-49-799287000-PDT.html [yegor] No arithT has no auto_tactics inside. It understands _,_,__,__,_ in hyps but_ Mon Sep 19 03:16:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-58-389775000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-58-389775000-PDT.html [xiny] Redefined subgroups. Now subgroup__g_ _s_ is a _type_ where _s is the_ Mon Sep 19 03:16:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-58-870168000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-16-58-870168000-PDT.html [yegor] Correct proof for _test__ Mon Sep 19 03:17:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-00-676119000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-00-676119000-PDT.html [yegor] When I removed .prlb and downloaded old .prla from CVS, mp does not showed_ Mon Sep 19 03:17:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-01-245541000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-01-245541000-PDT.html [nogin] Minor clean_up._ Mon Sep 19 03:17:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-05-831696000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-05-831696000-PDT.html [yegor] A small comment added in anyArithRel2geT_ Mon Sep 19 03:17:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-07-314382000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-07-314382000-PDT.html [xiny] Added _is_dep0_dep0_dep0_dep0_term_, _mk_dep0_dep0_dep0_dep0_term_,_ Mon Sep 19 03:17:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-24-509184000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-24-509184000-PDT.html [xiny] Added definition for equivalence relations, which are more general_ Mon Sep 19 03:17:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-24-998562000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-24-998562000-PDT.html [xiny] Replaced equality relations with equivalence relations everywhere in the_ Mon Sep 19 03:17:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-27-771082000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-27-771082000-PDT.html [xiny] Added czf_itt_equiv to MPFILES_ Mon Sep 19 03:17:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-29-985759000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-29-985759000-PDT.html [yegor] On the way to process relations in conclusion._ Mon Sep 19 03:17:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-30-351286000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-30-351286000-PDT.html [nogin] String_util cleanup__ Mon Sep 19 03:17:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-30-788234000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-17-30-788234000-PDT.html [nogin] esquash_mem does not have to be primitive, it follows directly from esquash_elim_ Mon Sep 19 03:18:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-18-04-577564000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-02/2005-09-19-03-18-04-577564000-PDT.html