src/HOL/Complex/NSComplexArith0.ML
2003-12-23 paulson 2003-12-23 type hcomplex is now in class field
2003-05-05 paulson 2003-05-05 new session Complex for the complex numbers