--- a/Paper/Paper.thy	Thu Jan 24 17:15:42 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 17:40:04 2013 +0100
@@ -550,7 +550,7 @@
   \begin{center}
   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
   \begin{tabular}[t]{@ {}l@ {}}
-  @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\
+  @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\[1mm]
   \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
   \hspace{7mm}if @{term "P (l, r)"} holds then\\
   \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
@@ -558,7 +558,7 @@
   \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
   \end{tabular} &
   \begin{tabular}[t]{@ {}l@ {}}
-  @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\
+  @{thm (lhs) Hoare_unhalt_def} @{text "\<equiv>"}\\[1mm]
   \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ 
   \hspace{7mm}if @{term "P (l, r)"} holds then\\
   \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"}
@@ -586,7 +586,7 @@
   \noindent
   {\it unfold} The first states that on a tape @{term "(Bk \<up> n,  [Oc, Oc])"}
   halts in tree steps leaving the tape unchanged. In the other states
-  that @{term dither} started with tape @{term "(Bk \<up> n,  [Oc, Oc])"} loops.
+  that @{term dither} started with tape @{term "(Bk \<up> n,  [Oc])"} loops.
   
 
 

Binary file paper.pdf has changed