/[mojave]/metaprl/theories/czf/czf_itt_abel_group.mli
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3555 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 07:49:49 2002 UTC (19 years, 2 months ago) by xiny
File length: 723 byte(s)
Diff to previous 3544
Updated the definition and rules for abelian groups due to the adding
of "eqG".


Revision 3544 - (view) (download) (annotate) - [select for diffs]
Modified Sun Mar 24 07:43:47 2002 UTC (19 years, 3 months ago) by xiny
File length: 759 byte(s)
Diff to previous 3498
Changed the definition of abelian groups completely. An abelian
group is now defined under equivalence relations instead of equality
relations, and there is a reduction rule for it.


Revision 3498 - (view) (download) (annotate) - [select for diffs]
Modified Sun Feb 17 02:09:08 2002 UTC (19 years, 4 months ago) by xiny
File length: 40 byte(s)
Diff to previous 3404
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.


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