diff -r 5d1200c7a671 -r 180364256231 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Fri Oct 15 16:44:37 1999 +0200
@@ -10,9 +10,9 @@
 theory ExprCompiler = Main:;
 
 text {*
- This is a (quite trivial) example of program verification.  We model
- a compiler translating expressions to stack machine instructions, and
- prove its correctness wrt.\ evaluation semantics.
+ 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.
 *};
 
 
@@ -21,7 +21,7 @@
 text {*
  Binary operations are just functions over some type of values.  This
  is both for syntax and semantics, i.e.\ we use a ``shallow
- embedding''.
+ embedding'' here.
 *};
 
 types
@@ -42,8 +42,8 @@
   Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";
 
 text {*
- Evaluation (wrt.\ an environment) is defined by primitive recursion
- over the structure of expressions.
+ Evaluation (wrt.\ some environment of variable assignments) is
+ defined by primitive recursion over the structure of expressions.
 *};
 
 consts