--- a/doc-src/IsarTut/generated/Tutorial.tex	Thu Jun 20 18:23:46 2002 +0200
+++ b/doc-src/IsarTut/generated/Tutorial.tex	Thu Jun 20 18:23:58 2002 +0200
@@ -7,7 +7,15 @@
 }
 \isamarkuptrue%
 %
-\isamarkupchapter{Interaction and debugging%
+\isamarkupchapter{Technical issues%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Source texts%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Interaction and debugging%
 }
 \isamarkuptrue%
 %