changeset 41959 | b460124855b8 |
parent 41413 | 64cd30d6b0b8 |
child 42463 | f270e3e18be5 |
--- a/src/HOL/NSA/NSComplex.thy Sun Mar 13 22:24:10 2011 +0100 +++ b/src/HOL/NSA/NSComplex.thy Sun Mar 13 22:55:50 2011 +0100 @@ -1,7 +1,6 @@ -(* Title: NSComplex.thy - Author: Jacques D. Fleuriot - Copyright: 2001 University of Edinburgh - Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 +(* Title: HOL/NSA/NSComplex.thy + Author: Jacques D. Fleuriot, University of Edinburgh + Author: Lawrence C Paulson *) header{*Nonstandard Complex Numbers*}