diff -r f92bf6674699 -r 846c72206207 src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Mon Nov 02 11:43:02 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Mon Nov 02 13:58:19 2015 +0100
@@ -10,17 +10,16 @@
 imports Main
 begin
 
-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>
+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>
 
 
 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"
 
@@ -28,16 +27,15 @@
 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>
+  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
@@ -48,16 +46,15 @@
 
 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
@@ -75,8 +72,8 @@
 
 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
@@ -85,9 +82,8 @@
 | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
 
 
-text \<open>The main result of this development is the correctness theorem
-  for @{text compile}.  We first establish a lemma about @{text exec}
-  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 =
@@ -127,11 +123,14 @@
 qed
 
 
-text \<open>\bigskip In the proofs above, the @{text simp} 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.\<close>
+text \<open>
+  \<^bigskip>
+  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.
+\<close>
 
 lemma exec_append':
   "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"