diff -r 480aae81b489 -r dfc629cd11de Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 03 12:24:28 2013 +0000
+++ b/Paper/Paper.thy	Sun Feb 03 13:31:14 2013 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/uncomputable"
+imports "../thys/abacus"
 begin
 
 (*
@@ -1119,9 +1119,6 @@
   to an contradiction, which means we have to abondon our assumption 
   that there exists a Turing machine @{term H} which can decide 
   whether Turing machines terminate.
-  
-
-
 *}
 
 
@@ -1135,22 +1132,22 @@
   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, but also
-  to refer to \emph{opcodes} of abacus 
-  machines. Obcodes are given by the datatype
+  to refer to \emph{statements} of abacus programs. Statements 
+  are given by the datatype
 
   \begin{center}
-  \begin{tabular}{rcll}
+  \begin{tabular}{rcl@ {\hspace{10mm}}l}
   @{text "o"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
   & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
   & & & then decrement it by one\\
-  & & & otherwise jump to opcode $o$\\
-  & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
+  & & & otherwise jump to statement $o$\\
+  & $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$
   \end{tabular}
   \end{center}
 
   \noindent
   A \emph{program} of an abacus machine is a list of such
-  obcodes. For example the program clearing the register
+  statements. For example the program clearing the register
   $R$ (setting it to 0) can be defined as follows:
 
   \begin{center}