| changeset 12674 | 106d62d106fc |
| parent 12673 | 90568836340a |
| child 12681 | 84188d1574ee |
--- 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}),