Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-11 13:56:41 -0800 (Tue, 11 Mar 2003)
Revision: 4163
Log message:
Xin & Aleksey:
- proved the subgroup intersection theorem (very straightforward,
but long proof with a lot of subcases)
- for ... >- f a in A, use intro in autoT
for ... >- f a = f' a' in A, only use intro with AutoMustComplete
- added type inference for group components
- added term contructors/descructors for the field term