# HG changeset patch
# User wenzelm
# Date 1024590238 -7200
# Node ID 52df43782fab97529db1ca326d12dc784b96100e
# Parent  031b119d265dc80eb02d9581a2bbd3ac7734b9e9
updated;

diff -r 031b119d265d -r 52df43782fab doc-src/IsarTut/generated/Tutorial.tex
--- 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%
 %