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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 3553 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 07:45:26 2002 UTC (19 years, 2 months ago) by xiny
File length: 1121 byte(s)
Diff to previous 3527
1. Added "eqG" to the definition of groups which denotes the equivalence
   relation related with the group. Every group has an equivalence
   relation, which is now explicitly described.
2. Accordingly, all rules related with equivalence relations in groups
   are updated and reproved.
3. Added tactics "uniqueInvLeftT" and "uniqueInvRightT" which might not
   be very useful though.


Revision 3527 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 4 02:20:01 2002 UTC (19 years, 3 months ago) by xiny
File length: 939 byte(s)
Diff to previous 3516
1. Replaced equality relations with equivalence relations in
   the definition axioms for "op", "inv", and "id".
2. Defined the equivalence functionality for "op" and "inv".
3. Changed the tactics for "left and right cancellation laws"
   (i.e., groupCancelLeftT and groupCancelRightT) to make it
   easier to use.
4. Re-proved all properties.


Revision 3516 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 25 02:24:42 2002 UTC (19 years, 4 months ago) by xiny
File length: 854 byte(s)
Diff to previous 3498
Replaced equality relations with equivalence relations everywhere in the
context of groups, and re-proved the rules.


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: 854 byte(s)
Diff to previous 3494
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 3494 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 7 23:19:33 2002 UTC (19 years, 4 months ago) by xiny
File length: 735 byte(s)
Diff to previous 3404
Removed tactics "op_assoc1T", "op_assoc2T" (previously as comments),
and "id_elim2T".


Revision 3404 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 23 07:25:28 2001 UTC (19 years, 9 months ago) by xiny
File length: 769 byte(s)
Diff to previous 3379
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.


Revision 3379 - (view) (download) (annotate) - [select for diffs]
Added Fri Sep 14 07:00:13 2001 UTC (19 years, 9 months ago) by xiny
File length: 735 byte(s)
Definition of algebraic group.


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