diff -r 2995639c6a09 -r 90695f46440b doc-src/TutorialI/CodeGen/CodeGen.thy --- a/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jan 12 16:28:14 2001 +0100 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jan 12 16:32:01 2001 +0100 @@ -2,7 +2,7 @@ theory CodeGen = Main: (*>*) -section{*Case study: compiling expressions*} +section{*Case Study: Compiling Expressions*} text{*\label{sec:ExprCompiler} The task is to develop a compiler from a generic type of expressions (built