ViewVC logotype

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

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: 741 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: 744 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: 702 byte(s)
Diff to previous 3495
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 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: 715 byte(s)
Diff to previous 3404
1. Changed the definition of cyclic groups to increase generality.
2. Added basic properties for the changed cyclic groups.

  The property "A subgroup of a cyclic group is cyclic" is not proven and
  might need to be re-defined.

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: 546 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