--- a/doc-src/TutorialI/Documents/document/Documents.tex Wed Aug 31 15:46:32 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Wed Aug 31 15:46:33 2005 +0200
@@ -898,7 +898,7 @@
\medskip Suppressing portions of printed text demands care. You
should not misrepresent the underlying theory development. It is
easy to invalidate the visible text by hiding references to
- questionable axioms.%
+ questionable axioms, for example.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- 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