# HG changeset patch
# User wenzelm
# Date 1010189686 -3600
# Node ID 3baa6143a9c4ddb565e6cee5223b999b1802fe9b
# Parent  ad9277743664a0b9ec1396eec86115bba52d7610
fixed \index;

diff -r ad9277743664 -r 3baa6143a9c4 doc-src/TutorialI/Types/Records.thy
--- 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|)}
 *}
 
 
diff -r ad9277743664 -r 3baa6143a9c4 doc-src/TutorialI/Types/document/Records.tex
--- 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%
 %