--- a/doc-src/TutorialI/Documents/Documents.thy Tue Jan 08 17:51:56 2002 +0100
+++ b/doc-src/TutorialI/Documents/Documents.thy Tue Jan 08 18:08:02 2002 +0100
@@ -654,7 +654,7 @@
*}
-subsection {* Interpretation of symbols \label{sec:doc-prep-symbols} *}
+subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
text {*
As has been pointed out before (\S\ref{sec:syntax-symbols}),
--- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 08 17:51:56 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Jan 08 18:08:02 2002 +0100
@@ -670,7 +670,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Interpretation of symbols \label{sec:doc-prep-symbols}%
+\isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
}
\isamarkuptrue%
%