--- a/Paper/Paper.thy	Tue Feb 05 08:57:55 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 08:58:30 2013 +0000
@@ -1221,7 +1221,7 @@
   one from @{term Bk} to @{term Oc}.
   Finally we need to transition the head of the
   Turing machine back into the standard position. This requires a Turing machine
-  with 9 states. Similarly for the translation of @{term Dec}, where the 
+  with 9 states (we omit the details). Similarly for the translation of @{term Dec}, where the 
   translated Turing machine needs to first check whether the content of the
   corresponding register is @{text 0}. For this we have a Turing machine program
   with @{text 16} states.