# 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: