--- a/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 26 15:50:28 2001 +0100
@@ -63,7 +63,7 @@
\begin{isamarkuptext}%
\noindent
Command \isacommand{typedecl} merely declares a new type but without
-defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+defining it (see \S\ref{sec:typedecl}). Thus we know nothing
about the type other than its existence. That is exactly what we need
because \isa{state} really is an implicit parameter of our model. Of
course it would have been more generic to make \isa{state} a type