--- a/Paper/Paper.thy	Thu Feb 07 00:46:04 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 00:48:09 2013 +0000
@@ -1160,10 +1160,10 @@
 
   \begin{center}
   \begin{tabular}{rcl@ {\hspace{10mm}}l}
-  @{text "i"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
-  & $\mid$ & @{term "Dec R\<iota> l"} & if content of $R$ is non-zero, then decrement it by one\\
-  & & & otherwise jump to instruction $l$\\
-  & $\mid$ & @{term "Goto l"} & jump to instruction $l$
+  @{text "i"} & $::=$  & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\
+  & $\mid$ & @{term "Dec R\<iota> l"} & if content of @{text R} is non-zero, then decrement it by one\\
+  & & & otherwise jump to instruction @{text l}\\
+  & $\mid$ & @{term "Goto l"} & jump to instruction @{text l}
   \end{tabular}
   \end{center}