diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/document/Base.tex --- 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