Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2003-02-23 23:36:05 -0800 (Sun, 23 Feb 2003)
Revision: 4118
Log message:
According to Alexei's comments:
1. Simplified the representation of {self : {record} | P[self]}
to {record; P[self]};
2. Changed the names of "G" and "e" to "car" and "1"; in the the extendend
syntax for records, removed quotes where labels are constant other than
"*" and "1".
3. Removed "group_is_monoid" from the intro resources.
Updated proofs accordingly.
TODO:
Need to work on improving the syntax and display forms of "*", "inv".
Alexei will work on the syntax part.