diff -r cc8aa63bdad6 -r 8016321c7de1 doc-src/TutorialI/CodeGen/document/CodeGen.tex
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Sep 05 13:12:00 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Sep 05 13:53:39 2000 +0200
@@ -1,8 +1,10 @@
 %
 \begin{isabellebody}%
 %
+\isamarkupsection{Case study: compiling expressions}
+%
 \begin{isamarkuptext}%
-\noindent
+\label{sec:ExprCompiler}
 The task is to develop a compiler from a generic type of expressions (built
 up from variables, constants and binary operations) to a stack machine.  This
 generic type of expressions is a generalization of the boolean expressions in