ViewVC logotype

Revision 3527

Jump to revision: Previous Next
Author: xiny
Date: Mon Mar 4 02:20:01 2002 UTC (19 years, 4 months ago)
Changed paths: 3
Log Message:
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.

Changed paths

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

  ViewVC Help
Powered by ViewVC 1.1.26