/[mojave]/metaprl/theories/czf/czf_itt_cyclic_group.ml
ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_cyclic_group.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3558 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 08:27:06 2002 UTC (19 years, 2 months ago) by xiny
File length: 1855 byte(s)
Diff to previous 3538
1. Changed the rewrite rule for cyclic groups. Previously it was defined
   by cyclic subgroups; now it is defined directly by its underlying set;
2. Updated rules due to the adding of "eqG" and reproved them.


Revision 3538 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 11 10:04:22 2002 UTC (19 years, 3 months ago) by xiny
File length: 2253 byte(s)
Diff to previous 3502
1. Changed the definition of cyclic groups from cyclic_group{'g;'a}
   which represented the carrier set of the cyclic group to
   cycgroup{'g; 'a} which is a "type" and can be rewritted as
   cyc_subg{'g; 'g; 'a};
2. Updated and proved rules about cyclic groups;
3. Added tactic "cycgroupAbelT".


Revision 3502 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 19 04:19:26 2002 UTC (19 years, 4 months ago) by xiny
File length: 3169 byte(s)
Diff to previous 3496
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.


Revision 3496 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 8 01:58:08 2002 UTC (19 years, 4 months ago) by xiny
File length: 3469 byte(s)
Diff to previous 3495
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.


Revision 3495 - (view) (download) (annotate) - [select for diffs]
Modified Fri Feb 8 01:06:03 2002 UTC (19 years, 4 months ago) by xiny
File length: 4378 byte(s)
Diff to previous 3486
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.


Revision 3486 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 30 02:01:20 2002 UTC (19 years, 4 months ago) by xiny
File length: 1677 byte(s)
Diff to previous 3404
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.


Revision 3404 - (view) (download) (annotate) - [select for diffs]
Added Sun Sep 23 07:25:28 2001 UTC (19 years, 9 months ago) by xiny
File length: 863 byte(s)
1. Minor changes in czf_itt_group;
2. Define subgroup and abelian group;
3. Define cyclic subgroup and cyclic group. However, there are
   problems with the proofs in czf_itt_cyclic_subgroup.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26