diff -r 30d81499766b -r 763ed488fa79 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 05 15:23:10 2013 +0000
+++ b/Paper/Paper.thy	Wed Mar 06 00:59:18 2013 +0000
@@ -1394,7 +1394,9 @@
   function for Church numbers, and also from Asperti and Ricciotti 
   \cite{AspertiRicciotti12} who construct a universal Turing machine
   directly, but for simulating Turing machines with a more restricted alphabet.
-  \emph{Recursive functions} are defined as the datatype
+  Unlike Norrish \cite{Norrish11}, we need to represent recursive functions
+  ``deeply'' because we want to translate them to abacus programs.
+  Thus \emph{recursive functions} are defined as the datatype
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{4mm}}c}