diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Expr_Compiler.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
 Correctness of a simple expression/stack-machine compiler.
 *)
@@ -10,32 +10,40 @@
 imports Main
 begin
 
-text \<open>This is a (rather trivial) example of program verification. We model a
+text \<open>
+  This is a (rather trivial) example of program verification. We model a
   compiler for translating expressions to stack machine instructions, and
-  prove its correctness wrt.\ some evaluation semantics.\<close>
+  prove its correctness wrt.\ some evaluation semantics.
+\<close>
 
 
 subsection \<open>Binary operations\<close>
 
-text \<open>Binary operations are just functions over some type of values. This is
-  both for abstract syntax and semantics, i.e.\ we use a ``shallow
-  embedding'' here.\<close>
+text \<open>
+  Binary operations are just functions over some type of values. This is both
+  for abstract syntax and semantics, i.e.\ we use a ``shallow embedding''
+  here.
+\<close>
 
 type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
 
 
 subsection \<open>Expressions\<close>
 
-text \<open>The language of expressions is defined as an inductive type,
-  consisting of variables, constants, and binary operations on expressions.\<close>
+text \<open>
+  The language of expressions is defined as an inductive type, consisting of
+  variables, constants, and binary operations on expressions.
+\<close>
 
 datatype (dead 'adr, dead 'val) expr =
     Variable 'adr
   | Constant 'val
   | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
 
-text \<open>Evaluation (wrt.\ some environment of variable assignments) is defined
-  by primitive recursion over the structure of expressions.\<close>
+text \<open>
+  Evaluation (wrt.\ some environment of variable assignments) is defined by
+  primitive recursion over the structure of expressions.
+\<close>
 
 primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
 where
@@ -46,15 +54,19 @@
 
 subsection \<open>Machine\<close>
 
-text \<open>Next we model a simple stack machine, with three instructions.\<close>
+text \<open>
+  Next we model a simple stack machine, with three instructions.
+\<close>
 
 datatype (dead 'adr, dead 'val) instr =
     Const 'val
   | Load 'adr
   | Apply "'val binop"
 
-text \<open>Execution of a list of stack machine instructions is easily defined as
-  follows.\<close>
+text \<open>
+  Execution of a list of stack machine instructions is easily defined as
+  follows.
+\<close>
 
 primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
 where
@@ -72,8 +84,10 @@
 
 subsection \<open>Compiler\<close>
 
-text \<open>We are ready to define the compilation function of expressions to
-  lists of stack machine instructions.\<close>
+text \<open>
+  We are ready to define the compilation function of expressions to lists of
+  stack machine instructions.
+\<close>
 
 primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
 where
@@ -82,8 +96,10 @@
 | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
 
 
-text \<open>The main result of this development is the correctness theorem for
-  \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.\<close>
+text \<open>
+  The main result of this development is the correctness theorem for
+  \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.
+\<close>
 
 lemma exec_append:
   "exec (xs @ ys) stack env =
@@ -128,8 +144,8 @@
   In the proofs above, the \<open>simp\<close> method does quite a lot of work behind the
   scenes (mostly ``functional program execution''). Subsequently, the same
   reasoning is elaborated in detail --- at most one recursive function
-  definition is used at a time. Thus we get a better idea of what is
-  actually going on.
+  definition is used at a time. Thus we get a better idea of what is actually
+  going on.
 \<close>
 
 lemma exec_append':