# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360529768 0
# Node ID 8a3e631639104d682bdea42072a6decd0362fb71
# Parent  67063c5365e18d77ef53b9482bbb8fe40a17fa2c
fixed compilation of paper and typo

diff -r 67063c5365e1 -r 8a3e63163910 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 10 19:49:07 2013 +0000
+++ b/Paper/Paper.thy	Sun Feb 10 20:56:08 2013 +0000
@@ -1296,7 +1296,7 @@
   \begin{center}
   \begin{tabular}{c@ {\hspace{4mm}}c}
   \begin{tabular}{rcl@ {\hspace{4mm}}l}
-  @{term r} & @{text "::="} & @{term z} & (zero-functions)\\
+  @{term r} & @{text "::="} & @{term z} & (zero-function)\\
             & @{text "|"}   & @{term s} & (successor-function)\\
             & @{text "|"}   & @{term "id n m"} & (projection)\\
   \end{tabular} &
diff -r 67063c5365e1 -r 8a3e63163910 Paper/ROOT.ML
--- a/Paper/ROOT.ML	Sun Feb 10 19:49:07 2013 +0000
+++ b/Paper/ROOT.ML	Sun Feb 10 20:56:08 2013 +0000
@@ -1,9 +1,9 @@
 no_document 
-use_thys ["../thys/turing_basic", 
-          "../thys/turing_hoare",
-          "../thys/uncomputable", 
-          "../thys/abacus"(*,
-          "../thys/rec_def",
-          "../thys/recursive"*)];
+use_thys ["../thys/Turing", 
+          "../thys/Turing_Hoare",
+          "../thys/Uncomputable", 
+          "../thys/Abacus",
+          "../thys/Rec_Def",
+          "../thys/Recursive"];
 
 use_thys ["Paper"]
diff -r 67063c5365e1 -r 8a3e63163910 paper.pdf
Binary file paper.pdf has changed