# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1362531558 0
# Node ID 763ed488fa79e7dec5e5e7e72d14e230f2b95792
# Parent  30d81499766b5fa2e30dc14204807a54b9ffc9ee
added a comment about deeply embedding of recursive functions

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}
diff -r 30d81499766b -r 763ed488fa79 paper.pdf
Binary file paper.pdf has changed