diff -r 892a3d7493aa -r 844e149696d4 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Feb 05 09:17:06 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 09:22:56 2013 +0000
@@ -1170,7 +1170,10 @@
   Turing machines, we fetch instructions from an abacus program such
   that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
   this way it is easy to define a function @{term steps} that
-  executes @{term n} instructions of an abacus program. By convention
+  executes @{term n} instructions of an abacus program. A \emph{configuration}
+  of an abacus machine is the program counter together with a snapshot of 
+  all registers.
+  By convention
   the value calculated by an abacus program is stored in the
   last register (the register with the highest index).
   
@@ -1244,7 +1247,10 @@
   use our Hoare-rules for reasoning about sequentially composed
   programs. Instead we have to treat the Turing machine as one ``block''
   and show as invariant that it performs the same operations
-  as the abacus program.
+  as the abacus program. For this we have to show that for each 
+  configuration of an abacus machine the @{term step}-function
+  is simulated by zero or more steps in our constructed Turing
+  machine. 
 
 
 *}