# HG changeset patch
# User wenzelm
# Date 928611510 -7200
# Node ID c68035d06cce6d03133aa56fbe0b15bc1935cf92
# Parent  2be411437c602df7f88c95c175b8e4f8e0df7742
tuned comments;

diff -r 2be411437c60 -r c68035d06cce src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Sat Jun 05 20:37:29 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Sat Jun 05 21:38:30 1999 +0200
@@ -13,8 +13,8 @@
 section {* Basics *};
 
 text {*
-  First we define a type abbreviation for binary operations over some
-  type @{type "'val"} of values.
+ First we define a type abbreviation for binary operations over some
+ type @{type "'val"} of values.
 *};
 
 types
@@ -24,7 +24,7 @@
 section {* Machine *};
 
 text {*
-  Next we model a simple stack machine, with three instructions.
+ Next we model a simple stack machine, with three instructions.
 *};
 
 datatype ('adr, 'val) instr =
@@ -33,8 +33,8 @@
   Apply "'val binop";
 
 text {*
-  Execution of a list of stack machine instructions is
-  straight-forward.
+ Execution of a list of stack machine instructions is
+ straight-forward.
 *};
 
 consts
@@ -56,8 +56,8 @@
 section {* Expressions *};
 
 text {*
-  We introduce a simple language of expressions: variables ---
-  constants --- binary operations.
+ We introduce a simple language of expressions: variables ---
+ constants --- binary operations.
 *};
 
 datatype ('adr, 'val) expr =
@@ -66,7 +66,7 @@
   Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";
 
 text {*
-  Evaluation of expressions does not do any unexpected things.
+ Evaluation of expressions does not do any unexpected things.
 *};
 
 consts
@@ -81,8 +81,8 @@
 section {* Compiler *};
 
 text {*
-  So we are ready to define the compilation function of expressions to
-  lists of stack machine instructions.
+ So we are ready to define the compilation function of expressions to
+ lists of stack machine instructions.
 *};
 
 consts
@@ -95,8 +95,8 @@
 
 
 text {*
-  The main result of this developement is the correctness theorem for
-  @{term "comp"}.  We first establish some lemmas.
+ The main result of this development is the correctness theorem for
+ @{term "comp"}.  We first establish some lemmas.
 *};
 
 lemma exec_append: