Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-01-20 17:17:09 -0800 (Tue, 20 Jan 2004)
Revision: 5265
Log message:
Defined unit ring.
Note: There might be a better way to formalize "isUnit" and the theorem
"the set of units forms a group under multiplication."