# HG changeset patch
# User wenzelm
# Date 1010509682 -3600
# Node ID 106d62d106fc3849e987001b9a8437ef7fc03dc0
# Parent  90568836340a326f60149c7ff5ed4f7b45c83a85
tuned;

diff -r 90568836340a -r 106d62d106fc doc-src/TutorialI/Documents/Documents.thy
--- 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}),
diff -r 90568836340a -r 106d62d106fc doc-src/TutorialI/Documents/document/Documents.tex
--- 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%
 %