# HG changeset patch
# User wenzelm
# Date 1125495993 -7200
# Node ID d26778f3e6dd2013484a42297f2713e9d95ce271
# Parent  24df6a93517c4bd3e909a1407e27e5eff72af58e
tuned;

diff -r 24df6a93517c -r d26778f3e6dd doc-src/TutorialI/Documents/document/Documents.tex
--- 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%
 %
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