ViewVC logotype

Revision 3530

Jump to revision: Previous Next
Author: xiny
Date: Thu Mar 7 23:13:10 2002 UTC (19 years, 4 months ago)
Changed paths: 2
Log Message:
1. Added properties that "e * a = a * e" and "a * e = e * a".
2. Changed the definition of groups to one-sided (left) definition,
   i.e., groups are defined by the left axioms, and proved the right
3. Removed the introduction forms of group cancellation laws which
   were put in comments in the last version.

Changed paths

Path Details
Directorymetaprl/theories/czf/czf_itt_group.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_group.prla modified , text changed

  ViewVC Help
Powered by ViewVC 1.1.26