--- a/Paper.thy	Thu Jan 10 11:27:45 2013 +0000
+++ b/Paper.thy	Thu Jan 10 11:28:26 2013 +0000
@@ -399,9 +399,9 @@
   \begin{center}
   \begin{tabular}{rcll}
   @{text "o"} & $::=$  & @{term "Inc R"} & increment register $R$ by one\\
-  & $\mid$ & @{term "Dec R o"} & if content of $R$ is non-zero, then decrement it by one\\
-  & & & otherwise jump to opcode $o$
-  & $\mid$ & @{term "Goto o"} & jump to opcode $o$
+  & $\mid$ & @{term "Dec R n"} & if content of $R$ is non-zero, then decrement it by one\\
+  & & & otherwise jump to opcode $o$\\
+  & $\mid$ & @{term "Goto n"} & jump to opcode $o$
   \end{tabular}
   \end{center}
 *}