diff -r bfe45b716dfc -r 2fbe5ce9845f src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 05 18:16:26 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 05 18:16:41 1999 +0200
@@ -7,7 +7,7 @@
 
 theory ExprCompiler = Main:;
 
-title {* Correctness of a simple expression/stack-machine compiler *};
+chapter {* Correctness of a simple expression/stack-machine compiler *};
 
 
 section {* Basics *};