src/HOL/NSA/NSComplex.thy
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*}