diff -r 2cae8a39803e -r c3155e9e4f63 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Feb 01 01:34:37 2013 +0000
+++ b/Paper/Paper.thy	Fri Feb 01 10:14:09 2013 +0000
@@ -928,9 +928,10 @@
   \hline
   \end{tabular}
   \end{center}
-  \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} for the states of 
-  @{term tcopy_begin}. Below, the invariants for the starting and halting states of
-  @{term tcopy_loop} and @{term tcopy_end}. In each invariant the parameter @{term n} stands for the number
+  \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of 
+  @{term tcopy_begin}. Below, the invariants only for the starting and halting states of
+  @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant the parameter 
+  @{term n} stands for the number
   of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
   \end{figure}
 
@@ -956,16 +957,18 @@
 
   We next need to show that @{term "tcopy_begin"} terminates. For this
   we introduce lexicographically ordered pairs @{term "(n, m)"}
-  derived from configurations @{text "(s, (l, r))"}: @{text n} stands
-  for the state ordered according to how @{term tcopy_begin} executes
-  them, that is @{text "1 > 2 > 3 > 4 > 0"}; @{term m} is calculated
-  according to the measure function:
+  derived from configurations @{text "(s, (l, r))"}: @{text n} is
+  the state @{text s}, but ordered according to how @{term tcopy_begin} executes
+  them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have
+  a strictly decreasing meansure, @{term m} takes the data on the tape into
+  account and is calculated according to the measure function:
 
   \begin{center}
   \begin{tabular}{rcl}
   @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & 
   @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\
-  & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} @{thm (rhs) measure_begin_print(2)} \\
+  & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} 
+  @{text "("}@{thm (rhs) measure_begin_print(2)}@{text ")"} \\
  & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\
   & & @{text else} @{thm (rhs) measure_begin_print(4)}\\
   \end{tabular}
@@ -974,9 +977,9 @@
   \noindent
   With this in place, we can show that for every starting tape of the
   form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing
-  machine @{term "tcopy_begin"} will halt. Taking this and the partial
-  correctness proof together we obtain for @{term tcopy_begin} (similar 
-  resoning is needed for @{term tcopy_loop} and @{term tcopy_end}):
+  machine @{term "tcopy_begin"} will eventually halt. Taking this and the partial
+  correctness proof together, we obtain for @{term tcopy_begin} the Hoare-triple
+  (similar resoning is needed for @{term tcopy_loop} and @{term tcopy_end}):
    
 
   \begin{center}
@@ -986,9 +989,12 @@
   \end{center}
 
   \noindent 
-  where we assume @{text "0 < n"}. Since @{term "inv_begin0 n \<mapsto> inv_loop1 n"} holds
-  and @{term "inv_loop0 n = inv_end1 n"}, we can derive using our Hoare-rules
-  the correctness of @{term tcopy}
+  where we assume @{text "0 < n"}. Since the invariant of the halting
+  state of @{term tcopy_begin} implies the invariant of the starting
+  state of @{term tcopy_loop}, that is @{term "inv_begin0 n \<mapsto>
+  inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1 n"}, we
+  can derive using our Hoare-rules for sequentially composed Turing programs
+  the correctness of @{term tcopy}:
 
   \begin{center}
   @{thm tcopy_correct}
@@ -1004,17 +1010,22 @@
   \end{center}
 
   \noindent
-  This means we considering only Turing machine programs representing functions that take 
-  some numbers as input and produce a single number as output. There is no Turing
-  machine that can decide the halting problem (answer @{text 0} for halting and 
-  @{text 1} for looping). Given our correctness proofs for @{term dither} and @{term tcopy} 
-  this non-existence is relatively straightforward to establish. We first assume there is a coding 
-  function, written @{term code}, from Turing machine programs to natural numbers.
-  Suppose a Turing machine @{term H} exists such that if started with the standard 
-  tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0} or @{text 1} depending
-  on whether @{text M} halts when started with the input tape containing @{term "<ns>"}.
-  This is formalised as follows
- 
+  This means we considering only Turing machine programs representing
+  functions that take some numbers as input and produce a single
+  number as output. The undecidability problem states that there is no
+  Turing machine that can decide the halting problem (answer eith
+  @{text 0} for halting and @{text 1} for looping). Given our
+  correctness proofs for @{term dither} and @{term tcopy} shown above,
+  this non-existence is relatively straightforward to establish. We
+  first assume there is a coding function, written @{term "code M"}, which
+  represents a Turing machine @{term "M"} as a natural number.  No further
+  assumptions are made about this coding function. Suppose a Turing
+  machine @{term H} exists such that if started with the standard tape
+  @{term "([Bk], <(code M, ns)>)"} returns @{text 0}, respectively @{text 1},
+  depending on whether @{text M} halts when started with the input
+  tape containing @{term "<ns>"}.  This assumption is formalised as 
+  follows---for all @{term M} and natural numbers @{term ns}:
+
   \begin{center}
   \begin{tabular}{r}
   @{thm (prem 2) uncomputable.h_case} implies