changeset 7740 | 2fbe5ce9845f |
parent 7565 | bfa85f429629 |
child 7748 | 5b9c45b21782 |
--- 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 *};