--- a/Paper.thy	Thu Jan 10 08:58:31 2013 +0000
+++ b/Paper.thy	Thu Jan 10 11:27:45 2013 +0000
@@ -3,7 +3,8 @@
 imports UTM
 begin
 
-hide_const (open) s
+hide_const (open) s 
+hide_const (open) R
 
 abbreviation 
   "update p a == new_tape a p"
@@ -384,6 +385,28 @@
 
 section {* Abacus Machines *}
 
+text {*
+  \noindent
+  Boolos et al \cite{Boolos87} use abacus machines as a 
+  stepping stone for making it less laborious to write
+  programs for Turing machines. Abacus machines operate
+  over an unlimited number of registers $R_0$, $R_1$, \ldots
+  each being able to hold an arbitrary large natural number.
+  We use natural numbers to refer to registers and also
+  to \emph{opcodes} of abacus machines. Obcodes are
+  defined as the datatype
+
+  \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$
+  \end{tabular}
+  \end{center}
+*}
+
+
 section {* Recursive Functions *}
 
 section {* Wang Tiles\label{Wang} *}