--- a/doc-src/TutorialI/Types/Records.thy Fri Jan 04 19:29:30 2002 +0100
+++ b/doc-src/TutorialI/Types/Records.thy Sat Jan 05 01:14:46 2002 +0100
@@ -213,7 +213,8 @@
than three consecutive periods, ``@{text "..."}''. Mixing the ASCII
and symbolic versions causes a syntax error. (The two versions are
more distinct on screen than they are on paper.)
- \end{warn}%\index{records!extensible|)}
+ \end{warn}%
+ \index{records!extensible|)}
*}
--- a/doc-src/TutorialI/Types/document/Records.tex Fri Jan 04 19:29:30 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Records.tex Sat Jan 05 01:14:46 2002 +0100
@@ -212,7 +212,8 @@
than three consecutive periods, ``\isa{{\isachardot}{\isachardot}{\isachardot}}''. Mixing the ASCII
and symbolic versions causes a syntax error. (The two versions are
more distinct on screen than they are on paper.)
- \end{warn}%\index{records!extensible|)}%
+ \end{warn}%
+ \index{records!extensible|)}%
\end{isamarkuptext}%
\isamarkuptrue%
%