--- a/src/HOL/Complex/ex/document/root.tex Wed Aug 31 15:46:32 2005 +0200
+++ b/src/HOL/Complex/ex/document/root.tex Wed Aug 31 15:46:33 2005 +0200
@@ -9,7 +9,7 @@
\begin{document}
-\title{Miscellaneous HOL-Hyperreal Examples}
+\title{Miscellaneous HOL-Complex Examples}
\maketitle
\tableofcontents