diff -r 24df6a93517c -r d26778f3e6dd src/HOL/Complex/ex/document/root.tex
--- 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