# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360198089 0
# Node ID 21c7139ffa07301eb989fdcfa3911ce7945dc55f
# Parent  4d7a568bd91177b8116c882daeb1bb5b463f1c02
updated paper

diff -r 4d7a568bd911 -r 21c7139ffa07 Paper/Paper.thy
--- 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}