diff -r 8dc659af1bd2 -r 4c8325c64dab Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Jan 25 22:12:01 2013 +0000
+++ b/Paper/Paper.thy	Sat Jan 26 01:36:48 2013 +0000
@@ -531,16 +531,19 @@
   We often need to restrict tapes to be in \emph{standard form}, which means 
   the left list of the tape is either empty or only contains @{text "Bk"}s, and 
   the right list contains some ``clusters'' of @{text "Oc"}s separted by single 
-  blanks and can be followed by some blanks. To make this formal we define the 
-  following function
+  blanks. To make this formal we define the following function
   
   \begin{center}
-  foo
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{thm (lhs) tape_of_nat_list.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(1)}\\
+  @{thm (lhs) tape_of_nat_list.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(2)}\\
+  @{thm (lhs) tape_of_nat_list.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list.simps(3)}
+  \end{tabular}
   \end{center}
 
   \noindent
-  A standard tape is then of the form @{text "(Bk\<^isup>k,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle> @ Bk\<^isup>l)"} for some @{text k},
-  @{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 
+  A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle>)"} for some @{text l} 
+  and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the 
   leftmost @{term "Oc"} on the tape.