src/HOL/Isar_examples/ExprCompiler.thy

--- a/src/HOL/Isar_examples/ExprCompiler.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Fri May 28 13:30:59 1999 +0200
@@ -7,12 +7,10 @@
 
 theory ExprCompiler = Main:;
 
-title
-  "Correctness of a simple expression/stack-machine compiler --- an Isabelle/Isar demonstration"
-  "Markus Wenzel";
+title {* Correctness of a simple expression/stack-machine compiler *};
 
 
-section "Basics";
+section {* Basics *};
 
 text {*
   First we define a type abbreviation for binary operations over some
@@ -23,7 +21,7 @@
   'val binop = "'val => 'val => 'val";
 
 
-section "Machine";
+section {* Machine *};
 
 text {*
   Next we model a simple stack machine, with three instructions.
@@ -55,7 +53,7 @@
   "execute instrs env == hd (exec instrs [] env)";
 
 
-section "Expressions";
+section {* Expressions *};
 
 text {*
   We introduce a simple language of expressions: variables ---
@@ -80,7 +78,7 @@
   "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
 
 
-section "Compiler";
+section {* Compiler *};
 
 text {*
   So we are ready to define the compilation function of expressions to
@@ -101,7 +99,6 @@
   @{term "comp"}.  We first establish some lemmas.
 *};
 
-
 lemma exec_append:
   "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
 proof (induct ??P xs type: list);
@@ -119,7 +116,6 @@
   qed;
 qed;
 
-
 lemma exec_comp:
   "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
 proof (induct ??P e type: expr);
@@ -133,7 +129,7 @@
 qed;
 
 
-text "Main theorem ahead.";
+text {* Main theorem ahead. *};
 
 theorem correctness: "execute (comp e) env = eval e env";
   by (simp add: execute_def exec_comp);